P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, & X. Rival, Why does Astrée scale up?

Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, & Xavier Rival.
Why does Astrée scale up?.
In Formal Methods in System Design 35(3):229—264, December 2009.
Paper:
- PDF (2.6 Mb)
Abstract:
ASTRÉE was the first static analyzer able to prove automatically the total absence of runtime errors of actual industrial programs of hundreds of thousand lines. What makes ASTRÉE such an innovative tool is its scalability, while retaining the required precision, when it is used to analyze a specific class of programs: that of reactive control-command software. In this paper, we discuss the important choice of algorithms and data-structures we made to achieve this goal. However, what really made this task possible was the ability to also take semantic decisions, without compromising soundness, thanks to the abstract interpretation framework. We discuss the way the precision of the semantics was tuned in ASTRÉE in order to scale up, the differences with some more academic approaches and some of the dead-ends we explored. In particular, we show a development process which was not specific to the particular usage ASTRÉE was built for, hoping that it might prove helpful in building other scalable static analyzers.
Keywords:
Abstract Interpretation, Embedded critical software, Formal methods, Safety, Scalability, Static analysis tool, Verification.
The is an extended paper version of the invited talk Numerical Domains for Software Verification By Abstract Interpretation of Patrick Cousot at the first international workshop on Numerical Abstractions for Software Verification (NSV'08), Princeton, July 8th, 2008.

Bibliographic reference:

\bibitem{CousotEtAl10-FMSD}
P.~Cousot, R.~Cousot, J.~Feret, L.~Mauborgne, A.~Min\'e, \& X.~Rival.
\newblock Why does Astrée scale up?.
\newblock In \emph{Formal Methods in System Design}, 35(3):229--264, December 2009.

@article{CousotEtAl10-FMSD,
   author =    {P{.} Cousot and R{.} Cousot and J.~Feret and L.~Mauborgne 
                and A.~Min\'e and X.~Rival},
   title =     {Why does Astrée scale up?},
   journal =   {Formal Methods in System Design},
   volume =    {35},
   number =    {3},
   year =      2009,
   month =     dec,
   pages =     {229--264},
   doi =       {10.1007/s10703-009-0089-6},
}

copyright notice, Springer copyright notice
Ba Last modified: Tuesday, 22-Feb-2011 17:44:44 CET