P. Cousot, Software Verification by Abstract Interpretation and the ASTRÉE Static Analyzer

Patrick Cousot.
Software Verification by Abstract Interpretation and the ASTRÉE Static Analyzer.
Seminar, Center for Computational and Systems Biology (COSBI), The Microsoft Research — University of Trento, Trento, Italy. February 5^th, 2008.
Abstract:
Abstract interpretation is a theory of sound approximation of the behavior of dynamic systems, in particular the semantics of programming languages. This is the formal basis for automatic correctness proofs by static analysers considering an over-approximation of the set of all possible executions of the program. Contrary to bug-finding methods (e.g. by test, bounded model-checking or error pattern search), no potential error is ever omitted. Hence the proof of satisfaction of a specification is always mathematically valid. Contrary to refinement-based methods, termination is always guaranteed. However, by undecidability of such proofs, the abstraction may yield false alarms whenever a synthesized inductive argument (e.g. a loop invariant) is too weak to make the proof. In this case, some executions considered in the abstract, that is in the over-approximation, might lead to an error while not corresponding to a concrete, that is actual, execution. All the difficulty of the undecidable verification problem is therefore to design safe/sound over-approximations that are coarse enough to be effectively computable by the static analyzer and precise enough to avoid false alarms (the errors leading to true alarms can only be eliminated by correcting the program that does not satisfy the specification).
After a brief introduction to abstract interpretation, we will present the ASTRÉE static analyser (www.astree.ens.fr) for proving the absence of runtime errors (such as buffer overrun, dangling pointer, division by zero, float overflow, modular integer arithmetic overflow, ...) in real-time synchronous control/command C applications. The ASTRÉE static analyser uses generalist abstractions (like intervals, octagons, decision trees, symbolic execution, etc) and abstractions for the specific application domain (to cope with filters, integrators, slow divergences due to rounding errors, etc). Since 2003, these domain-specific abstractions allowed for the verification of the absence of RTEs in several large avionic software, a world première.
Slides of the 55 mn presentation: .pdf .

Bibliographic reference:

\bibitem{Cousot-Trento-2008-02-05}
P.~Cousot.
\newblock Software Verification by Abstract Interpretation and the 
         \textsc{As\-tr{\'e}e} Static Analyzer.
\newblock \emph{seminar}, Center for Computational and Systems Biology (COSBI), 
          The Microsoft Research -- University of Trento, Trento, Italy, 
          February 5${^\mathrm{th}}$ 2008.


@inProceedings{Cousot-08-02-05-COSBI-Trento,
   author =    {P{.} Cousot},
   title =     {Software Verification by Abstract Interpretation 
                and the \textsc{As\-tr{\'e}e} Static Analyzer},
   booktitle = {Seminar, Center for Computational and Systems Biology 
                (COSBI)}, 
   address =   {The Microsoft Research -- University of Trento, Italy},
   month =     {5 February},
   year =      {2008},
}

copyright notice
Last modified: Thursday, 05-Jul-2007 13:25:44 CEST