P. Cousot, Why Astrée does scale?

Patrick Cousot.
Why ASTRÉE does scale?
Dagstuhl seminar 08161, « Scalable Program Analysis », Schloss Dagstuhl, Germany April 15^th, 2008.
Abstract:
     ASTRÉE is an abstract-interpretation based static analyzer developped at ENS, Paris to prove the absence of run-time errors in C programs. It has proved useful in an industrial context to verify synchronous control/command software. It is sound, non-intrusive, precise, efficient and scales up.
     We describe the considered language, its concrete semantics, the implicit specification checked by ASTRÉE and sketch the internal structure, starting from the iterator. We describe trace partitionning, the memory model, the reduction between abstractions and a few typical abstract domains used by ASTRÉE.
     We then discuss how the cost/precision ratio of the analyses can be tuned through parameters, user directives and the automatic generation of these directives for well-identified families of application programs. We present in more detail the parameterized refinements through widening, variable packing, size limitation to avoid explosion, etc. We also discuss refinement by addition of new abstract domains when the cost/precision ratio cannot be tuned by parametrization of currently available abstractions. We conclude with a comparison with other static analyzers.
     In the demo session, we provide small pedagogic examples illustrating the main characteritics of ASTRÉE while analyzing an actual industrial avionic application.
Slides of the 60 mn presentation: .pdf.

Demonstration of ASTRÉE (20 mn) :.pdf

Bibliographic reference:

\bibitem{Cousot-Dagstuhl-2008-04-15}
P.~Cousot.
\newblock Why Astr\'ee does scale?
\newblock \emph{Dagstuhl seminar 08161, ``Scalable Program Analysis''}, 
           Schlo\ss\ Dagstuhl, Germany, April 15${^\mathrm{th}}$ 2008.

@inProceedings{Cousot-Dagstuhl-2008-04-15,
   author =    {P{.} Cousot},
   title =     {Why Astr\'ee does scale?},
   booktitle = {Dagstuhl seminar 08161, Scalable Program Analysis},
   address =   {Dipartimento di Matematica Pura ed Applicata, Universit{`a} degli Studi di Padova, Padova, Italy},
   month =     {February 19${^\mathrm{th}}$ 2008},
   year =      2008,
}

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