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, Computer Science Department, Stony Brook University, Stony Brook, New York, USA. January 18^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 runtime errors in several large avionic software, a world premi\`ere.
Slides of the 55 mn presentation: .pdf .

Bibliographic reference:

\bibitem{Cousot-SUNYSB-2008-01-18}
P.~Cousot.
\newblock Software Verification by Abstract Interpretation 
          and the \textsc{As\-tr{\'e}e} Static Analyzer.
\newblock \emph{Seminar}, Computer Science Department, State 
          University of New York at Stony Brook, USA.
          January 18${^\mathrm{th}}$ 2008.

@inProceedings{Cousot-08-01-18-StonyBrook,
   author =    {P{.} Cousot},
   title =     {Software Verification by Abstract Interpretation 
                and the \textsc{As\-tr{\'e}e} Static Analyzer},
   booktitle = {Seminar, Computer Science Department},
   address =   {State University of New York at Stony Brook\USA},
   month =     {18 January},
   year =      {2008},
}