École Jeunes Chercheurs en Programmation - École des Mines de Nantes - 23 mars au 2 avril 1998

Interprétation abstraite

Patrick Cousot

Mercredi 1er Avril 1998, 9h15 - 12h30 & 14h30 - 17h45.

Plan du cours :

• Introduction à l'analyse sémantique statique de programmes par interprétation abstraite [1];
• Spécification de propriétés de programmes par points fixes [2] ;
• Approximation de sémantiques par abstraction [3] ;
• Construction de hiérarchies de sémantiques par interprétation abstraite [3] ;
• Approximation effective de sémantiques par élargissement [4] ;
• Exemples d'analyses sémantiques par interprétation abstraite :
  • domaine de valeur des variables numériques [5],
  • domaine de valeur des variables non numériques [6],
  • analyse de nécessité, généralisation à l'analyse de comportement [7],
  • typage [8].

Références pour le cours :

1. Patrick Cousot. Abstract Interpretation. In ACM Computing Surveys, Vol. 28, No. 2, pages 324--328, June 1996.
2. Patrick Cousot & Radhia Cousot. Introduction to Abstract Interpretation, notes extraites de JLC 13(2--3):103--179, 1992.
3. Patrick Cousot. Constructive Design of a Hierarchy of Semantics of a Transition System by Abstract Interpretation. Electronic Notes in Theoretical Computer Science, 6 (1997) URL: http://www.elsevier.nl/locate/entcs/volume6.html, 25 pages.
4. Patrick Cousot & Radhia Cousot. Comparing the Galois connection and widening/narrowing approaches to abstract interpretation, invited paper. In M. Bruynooghe & M. Wirsing, editors, Programming Language Implementation and Logic Programming, Proceedings of the Fourth International Symposium, PLILP'92, Leuven, Belgium, 13--17 August 1992, Lecture Notes in Computer Science 631, pages 269--295. Springer-Verlag, Berlin, Germany, 1992.
5. N. Halbwachs, Y.E. Proy & P. Roumanoff. Verification of real-time systems using linear relation analysis, Formal Methods in System Design, Vol. 11, No. 2, pages 157-185, August 1997, Kluwer Pub. Co.
6. Patrick Cousot & Radhia Cousot. Formal Language, Grammar and Set-Constraint-Based Program Analysis by Abstract Interpretation. In Conference Record of FPCA '95 SIGPLAN/SIGARCH/WG2.8 Conference on Functional Programming and Computer Architecture, pages 170--181, La Jolla, California, U.S.A., 25-28 June 1995. ACM Press, New Y ork, U.S.A.
7. Patrick Cousot & Radhia Cousot. Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages), invited paper. In Proceedings of the 1994 International Conference on Computer Languages, ICCL'94, Toulouse, France, pages 95--112. IEEE Computer Society Press, Los Alamitos, California, U.S.A., May 16--19, 1994.
8. Patrick Cousot. Types as Abstract Interpretations, invited paper Conference Record of the 24th ACM SIGACT-SIGMOD-SIGART Symposium on Principles o f Programming Languages, Paris, France, 15--17 January 1997. ACM Press, New York, U.S.A. pp. 316-331.