Colloquia Patavina: Advances and Challenges in Static Program Analysis by Abstract Interpretation


Martedi' 19 Febbraio 2008 alle ore 16:00 in aula 1A/150 della Torre Archimede il Professor Patrick Cousot dell' École Normale Supérieure di Parigi terra' una conferenza della serie Colloquia Patavina dal titolo "Advances and Challenges in Static Program Analysis by Abstract Interpretation".

La Commissione Colloquia
M. A. Garuti, M. Pavon, M. Pitteri, F. Rossi

Advances and Challenges in Static Program Analysis by Abstract Interpretation

Patrick Cousot (École Normale Supérieure, Paris)

Martedi' 19 Febbraio 2008, ore 16:00
Aula: 1A/150, Torre Archimede

The correctness proof objective of formal methods is to show that a semantic model of the possible computations of a program satisfy a formal specification. Formal methods must confront various problems, including the definition of the semantics of programming and specification languages as well as the automation of undecidable proofs.
Abstract interpretation introduces the ideas of abstraction and approximation in formal methods which is mandatory to cope with complex software systems and undecidability. It formalizes the idea that sound reasonings on abstract models of program semantics should be valid on any concrete computation. It also provides completeness conditions for correctness proofs to succeed in the abstraction.
Abstract interpretation can be applied to the design of programming languages semantics, deductive methods, abstract model-checking, typing, static analysis, program transformation, and many other applications at various levels of abstraction.
Static analysis consists in proving that an abstraction of a program semantics (overapproximating all program computations) implies an implicit safety or security specification. The abstraction must be chosen to be sound, precise enough to imply the specification, and approximate enough to be cheaply representable and computable. By
undecidability, this approximation introduces spurious behaviors which can be at the origin of false alarms that is fictive violations of the specification.
The experience of ASTREE (, shows that static analyzers to prove the absence of runtime errors in safety critical synchronous real-time control/command software can be both sound, efficient and precise when applied to domain-specific family of programs. The challenge is to broaden the considered class of programs and properties.

-Breve curriculum
Patrick Cousot is Professor of Computer Science at the Ecole Normale Superieure, Paris, France, where he chairs the department's educational programme, and leads the Abstract Interpretation and Semantics research group associated to CNRS and INRIA (ASBTRACTION project-team). Professor Cousot is a renowned authority on semantics and static analysis of computer software, and the inventor of abstract interpretation.

Download Colloquia Patavina

Download ASTREE