(Patrick Cousot)

Reasonings on computer systems, whether purely intellectual or automatize, all require to have models of the behaviour of these computer systems at execution. The design of such mathematical models is the subject of the semantics of programming languages.

Depending upon the properties of interest of these computer systems, the model used as the basis for reasoning must be more or less concrete or refined (when one must take all details into account) or, on the contrary, more or less abstract (in order to do global reasonings ignoring irrelevant details).

Abstract interpretation is a theory of approximation which formalizes this notion of abstraction so as to design models of computer systems from existing ones by refinement or abstraction.

When the abstraction is coarse enough to be computable, one can derive typing, model-checking and static analysis algorithms from the semantics of the computer system which automatically provide information about the runtime execution of the system, without having to execute it.

Content of the course:

- Elements of order theory;

- Elements of fixpoint theory;

- Galois connections;

- Exact fixpoint abstraction;

- Application to the design of semantics by abstraction of the trace semantics;

- Constructive approximation of fixpoints;

- Type inference for the lambda-calculus by abstract interpretation;

- Design of model checking algorithms by abstract interpretation;

- Soundness and completeness of program proof methods;

- The lattice of abstract interpretations, examples.

Bibliography :

- P.Cousot. Types as abstract interpretations. In Conference Record of the Twentyfourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 316-331, Paris, France, January 1997. ACM Press, New York, NY, U.S.A.

- P. Cousot et R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 238-252, Los Angeles, California, 1977. ACM Press, New York, NY, USA.

- P.Cousot et R.Cousot. Systematic design of program analysis frameworks. In Conference Record of the Sixth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 269-282, San Antonio, Texas, 1979. ACM Press, New York, NY, U.S.A.

- P.Cousot et R.Cousot. Abstract Interpretation Frameworks. Journal of Logic and Computation, 2(4):511-547, August 1992.

- P.Cousot. Constructive Design of a Hierarchy of Semantics of a Transition System by Abstract Interpretation. Theoretical Computer Science 277(1-2):47-103, 2002.

- P.Cousot et R.Cousot. Temporal abstract interpretation. In Conference Record of the Twentyseventh Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 12-25, Boston, Mass., January 2000. ACM Press, New York, NY, U.S.A.