P. Cousot, ASTRÉE : A Static Analyzer for Large Safety-Critical Software

Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret Laurent Mauborgne, Antoine Miné, David Monniaux & Xavier Rival.
ASTRÉE : A Static Analyzer for Large Safety-Critical Software.
Applied Deductive Verification Schloss Dagstuhl Seminar 3451, 2—7 Nov. 2003.
Abstract:    Astrée is an abstract interpretation-based static analyzer that is efficient and precise enough to verify a class of properties in a family of large real-time embedded safety-critical applications with very few or no false alarms. This is achieved by refinement of a general- purpose static analyzer and later adaptation to particular programs of the family by the end- user through parameterization.
   The programs analyzed by Astrée compute logical and numerical values (floats and integers) of a huge number of variables. Although the programs are in a restricted family (absence of dynamic memory allocation), the problems raised by the precise analysis are quite challenging. Most variables are global (in such a number that no relational analysis of those variables is tractable) and the main body of the code is a big loop, which makes everything interdependent (and so prevents the reduction of the problems into smaller independent problems).
   In order to tackle these challenges, Astrée was designed following an original principle of static analyzers by refinement and adaptation through parameterization. During this process, Astrée was enriched with new domains, such as the ellipsoid or the filter domain, which can represent non-standard relational invariants, or the decision-tree abstract domain to deal with complex control flows. Other domains that were already presented in the literature, such as octagons, had to be enriched for a sound and precise handling of rounding errors in floating point computations. In order to improve the precision of the abstract transfer functions, the analyzer includes symbolic manipulation of expressions (sound for floating points) and partitioning of traces according to the control flow or the value of some integer variables. Finally, new widening strategies (with thresholds or delayed) had to be developed.
   Although the analyzer can be extensively parameterized by the end-user, Astrée provides the automatic determination of the parameters (parameterized packing).
   Astrée has been successfully used to prove the soundness of data manipulation operations at the machine level (including absence of any runtime error) for periodic synchronous safety-critical embedded software with no false alarm.
Slides of the 45mn talk: .pdf.gz

Bibliography:

\bibitem{BlanchetCousotEtAL-Dagstuhl-3451-2003}
B{.} Blanchet, P{.} Cousot, R{.} Cousot{.}, J. Feret, L{.} Mauborgne, 
A{.} Min\'e, D{.} Monniaux \& X{.} Rival.
\newblock {ASTR\'EE} : A Static Analyzer for Large Safety-Critical Software.
\newblock \emph{Schlo\ss\ Dagstuhl Seminar 3451}
          2--7 November, 2003.

@unpublished{BlanchetCousotEtAL-Dagstuhl-3451-2003,
   author =    {B{.} Blanchet and P{.} Cousot and R{.} Cousot{.} and J. Feret 
                and L{.} Mauborgne and A{.} Min\'e and D{.} Monniaux and 
                X{.} Rival},
   title =     {{ASTR\'EE} : A Static Analyzer for Large Safety-Critical Software},
   note = {Schlo\ss\ Dagstuhl Seminar 3451},
   month =     {2--7 November},
   year =      2003,
}

copyright notice.
Last modified: Monday, 07-May-2012 17:51:03 EDT