P. Cousot, Software Verification by Abstract Interpretation.

Patrick Cousot.
Software Verification by Abstract Interpretation.
School of Computer and Communication Sciences Seminar, École Polytechnique Fédérale de Lausanne (EPFL), Switzerland, december 10, 2007.

Abstract:
The difficulties with formal methods are that they need a formal specification, a formal semantics of the programming language and, because of undecidability, have serious limits in the automatic verification that the program semantics satisfies the specification. A theorem prover needs human assistance while model-checking requires finite models which, but for hardware, are generally incomplete.
Static analysis offers an interesting completely automatic alternative in that the specification can be chosen to be implicit. For example the absence of runtime error will not require the user to define a complex specification. Moreover static analysis considers infinite models of computations that can be directly computed from the program text so that the end-user does not need to provide a (finite) model of the program computations and environment. Finally, the reachable states during any program computation are computed approximately through an overapproximation that omits no possible case. So the delicate questions about the program semantics can be solved by considering all possible alternatives.
If this overapproximation copes with the undecidability problem, its inconvenience is that it considers spurious program behaviors, which do not exist in any actual execution, but may be at the origin of alarms, so-called ``false alarms''. This approach is sound in that no runtime error will ever be omitted in the diagnostic. It is incomplete, because of the potential false alarms. In general false alarms have to be solved by manual code inspection, which is extremely costly. The whole problem is therefore to choose abstractions of the program semantics that yield few or no alarm. To do so, one can restrict the family of programs to be analyzed to a specific application domain so as to adapt the abstraction exactly the domain-specific primitives and algorithmic schema found in this family of programs.
We will present elements of the theory of abstract interpretation on which the soundness of the notion of overapproximation does rely. Then we will introduce the ASTRÉE static analyzer (www.astree.ens.fr), which is specialized for the verification of the absence of runtime errors in control-command programs. The analyzer has general-purpose abstractions (e.g.\ octagons, control and data partitioning) as well as domain-specific abstractions (e.g.\ to handle filters or the potential accumulation of rounding errors). Finally, we will report on the successful application of ASTRÉE to the proof of absence of runtime errors in recent avionic flight control software.

The slides of the 60mn talk are available in PDF format, 4 slides per A4 landscape page, to be used Acrobat Reader
- pdf (2 Mb)

Bibliographic reference:

\bibitem{Cousot-EPFL07}
P.~Cousot.
\newblock Software Verification by Abstract Interpretation.
\newblock \emph{School of Computer and Communication Sciences Seminar},
           \'Ecole Polytechnique F\'ed\'erale de Lausanne (EPFL), 
           Switzerland, December 10, 2007.

@inProceedings{Cousot-EPFL07,
   author =    {P{.} Cousot},
   title =     {Software Verification by Abstract Interpretation},
   booktitle = {School of Computer and Communication Sciences Seminar},
   address =   {\'Ecole Polytechnique F\'ed\'erale de Lausanne (EPFL), 
                Switzerland},
   month =     {December 10},
   year =      2007,
}

copyright notice
Last modified: Monday, 04-Jan-2010 13:46:17 CET