P. Cousot, The ASTRÉE Static Analysis Tool.

Patrick Cousot.
The ASTRÉE Static Analysis Tool.
In ES_PASS Workshop, Berlin, Germany, 16--17 October 2007.
Abstract:
Software verification consists in proving that executions of the software in any admissible execution environment all satisfy a formal specification. In the case of the ASTRÉE static analyser (http://www.astree.ens.fr/), the specification is implicit: no execution can lead to a “runtime error” (RTE) (such as buffer overrun, dangling pointer, division by zero, float overflow, modular integer arithmetic overflow, etc). The ASTRÉE static analyser is designed by abstract interpretation of the semantics of a subset of the C programming language (without dynamic memory allocation, recursive function calls, no system and library calls as found in most embedded software). Abstract interpretation is a theory of abstraction, that is to say of safe approximation allowing for automatic formal proofs by 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 the specification is mathematically valid. However, 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. This spurious execution is then said to lead to a ``false alarmÕÕ. 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). In practice, knowing only the over-approximation computed by the static analyser, it is difficult to distinguish false alarms from actual ones. So the radical solution is to reach zero false alarm which provides a full verification. To do so, ASTRÉE is specialized both to precise program properties (i.e. RTEs) and a precise family of C programs (i.e. real-time synchronous control/command C applications preferably automatically generated from a synchronous language). 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.
The slides of the 25mn talk: .pdf (and in long version)

ASTRÉE Demo (http://www.astree.ens.fr/):
ASTRÉE (http://www.astree.ens.fr/) is a static analysis tool to prove the absence of runtime errors in real-time critical embedded synchronous control/command software which was applied with success to the verification of avionic software. The demonstration is on small representative examples of the application domain.

A typescript of the demo is available in PDF format (172 Kb).

Bibliographic references:

\bibitem{Cousot-ES_PASS-Berlin07}
P.~Cousot.
\newblock The \textsc{Astrée} Static Analysis Tool.
\newblock \emph{ES_PASS Workshop}, Berlin, Germany, 16--17 October 2007.

@inProceedings{-ES_PASS-Berlin07,
   author =    {P{.} Cousot},
   title =     {The \textsc{Astrée} Static Analysis Tool},
   booktitle = {ES_PASS Workshop},
   address =   {Berlin, Germany},
   month =     {16--17 October},
   year =      2007,
}

copyright notice
Last modified: Thursday, 07-Jun-2007 20:55:32 CEST