-
Patrick Cousot.
Interprétation Abstraite et Analyse Statique. 
Le LIX fète
ses dix ans, LIX, École polytechnique, 26 mai 1999.
- Résumé :
La croissance extraordinaire des capacités matérielles des
ordinateurs engendre une croissance comparable de la taille et de la
complexité des logiciels qu'ils peuvent mettre en œuvre. Les
capacités intellectuelles des informaticiens n'évoluant pas
sensiblement au fil des années et la taille des groupes de
développement et de maintenance des logiciels ne pouvant pas
croître dans de telles proportions, il paraît évident
que les méthodes actuelles de développement et
vérification de logiciels ne passent pas à l'échelle
quand on imagine les développements futurs possibles des
applications de l'informatique, en particulier pour les systèmes
dont la sécurité et la fiabilité est critique et la
validation est extrêmement complexe et coûteuse.
Seul l'emploi de l'ordinateur pour détecter les fautes dans les
programmes peut permettre de passer à l'échelle, par
automatisation partielle de la tâche de validation des programmes.
Les résultats classiques d'indécidabilité montrent que
les ordinateurs et leurs programmes n'ont pas les moyens de
s'auto-introspecter complètement de la sorte.
Nous expliquerons complètement informellement comment la
théorie de l'interprétation abstraite que nous avons
développée depuis une vingtaine d'années peut
être utilisée pour faire face à cette énorme
difficulté. Il s'agit d'une théorie de l'approximation de la
sémantique des programmes, où la sémantique
définit formellement tous les comportements possibles d'un programme
quand il est exécuté en interaction avec un environnement
quelconque. L'idée centrale est de considérer des notions
d'abstraction qui permettent d'en calculer une approximation de
manière effective. Du fait de la perte d'information, la
sémantique abstraite ne permet pas de répondre à
toutes les questions mais toutes les réponses données sont
justes, tous les cas possibles sont considérés et il est
possible de s'adapter au mieux aux propriérés pertinentes.
De nombreuses questions pratiques peuvent être abordées par
interprétation abstraite. Parmi les applications principales de la
théorie de l'interprétation abstraite, l'analyse statique,
qui fût la première application que nous avons
considérée, est maintenant passée au stade
d'industrialisation.
- Transparents : .pdf.gz. Le fichier PDF doit être dans un répertoire comprenant un sous-répertoire "songs"
contenant ce fichier son.
-
Patrick Cousot.
Abstract Interpretation and Static Analysis.
LIX ten years celebration, LIX, École polytechnique, 26 May 1999.
- Abstract:
The extraordinary development of the computer hardware capacities generates
a comparable growth of the size and complexity of the software they can
run. The intellectual capacity of the computer scientists does not evolve
significantly over years and the size of the development and maintenance
teams cannot grow in similar proportions. It seems therefore obvious that
the present software development and maintenance methods do not scale up
when thinking to the possible future developments of computer applications,
in particular for safety and security critical systems which validation is
extremely complex and costly.
The use of computers to detect program bugs might be the only way to scale
up by partial automatization of the program validation task.
undecidability results show that computers and their programs do not have
the necessary ability for such complete introspection.
We will explain completely informally how the theory of abstract
interpretation that we have pioneered and developed since twenty years, can
be used to cope with this extreme difficulty. This is a theory of
approximation of the semantics of programs. The semantics defines formally
all possible behaviors of a program when executed in interaction with any
possible environment. The central idea is to consider abstractions
allowing for the effective computation of precise enough approximations.
The information lost does not allow to answer all questions but all answers
are correct and all possible cases are considered. It is possible to adapt
the precision of the abstraction to the properties considered pertinent.
Numerous practical questions can be solved by abstract interpretation.
Among the main applications of the theory, static analysis, which was the
first application that we considered, is presently industrialized.
- Slides (in French) : .pdf.gz. The PDF file should be in a directory with a
subdirectory "songs" containg this sound file.