Abstract Interpretation and Application to the Static Analysis of Safety-Critical Embedded Computer Software

Abstract

Static software analysis has known brilliant successes in the small, by proving complex program properties of programs of a few dozen or hundreds of lines, either by systematic exploration of the state space or by interactive deductive methods. To scale up is a definite problem. Very few static analyzers are able to scale up to millions of lines without sacrificing automation and/or soundness and/or precision. Unsound static analysis may be useful for bug finding but is less useless in safety critical applications where the absence of bugs, at least of some categories of common bugs, should be formally verified.

After recalling the basic principles of abstract interpretation including the notions of abstraction, approximation, soundness, completeness, false alarm, etc., we introduce the domain-specific static analyzer ASTREE (www.astree.ens.fr) for proving the absence of runtime errors in safety critical real time embedded synchronous software in the large.

The talk emphasizes soundness (no runtime error is ever omitted), parametrization (the ability to refine abstractions by options and analysis directives), extensibility (the easy incorporation of new abstractions to refine the approximation), precision (few or no false alarms for programs in the considered application domain) and scalability (the analyzer scales to millions of lines).

In conclusion, present-day software engineering methodology, which is based on the control of the design, coding and testing processes should evolve in the near future, to incorporate a systematic control of final software product thanks to domain-specific analyzers that scale up.

Short bio

Patrick Cousot is Professor of Computer Science at the École Normale Supérieure (ENS, since 1991), Paris, France.

He is Director of the Computer Science educational activities and leads the research on abstract interpretation and semantics.

Before joigning the École Normale Supérieure, Patrick Cousot was successively, Research Scientist at the French National Center for Scientific Research (CNRS, 1974-1979), Professeur des Universités (University of Metz, 1979-1984), and Professor at the École Polytechnique (X, 1984-1997) where he developped the educational activities in Computer Science and created and headed the research laboratory (LIX).

Patrick Cousot was born on December 3rd, 1948. He is Engineer from École des Mines of Nancy (1971), Doctor Engineer (PhD) in Computer Science (1974) and Doctor ès Sciences in Mathematics (1978) from the University of Grenoble.

Patrick Cousot is the founder of Abstract Interpretation, a theory he developed in his Doctorate ès Sciences thesis. Abstract interpretation is a theory of sound approximation of mathematical structures, in particular those involved in the behavior of computer systems. It allows the systematic derivation of sound methods and algorithms for approximating undecidable or highly complex problems in various areas of computer science (semantics, verification and proof, model-checking, static analysis, program transformation and optimization, typing, software steganography, etc.). Its main current application is on the safety and security of complex hardware and software computer systems.

Patrick Cousot is Member of the Academia Europaea (2006). He was awarded the Grand Prix of Computer Science and its Applications of the EADS Corporate Research Foundation attributed by the French Academy of Sciences (2006), the Silver Medal of the CNRS (1999) for his seminal work on abstract interpretation, the honorary degree Dr.-Ing. E.h. from the Fakultät Mathematik und Informatik of the Universität des Saarlandes (2001), and the J. C. Hunsaker Distinguished Visiting Professor position at the Massachusetts Institute of Technology (MIT, 2005). He was named Chevalier (knight) in the Ordre National du Mérite and the Ordre des Palmes académiques.

Photos

Resources

• talk slide