P. Cousot, Automated Verification of Infinite-State Systems by Abstract Interpretation

Patrick Cousot.
Automated Verification of Infinite-State Systems by Abstract Interpretation.
In Third International Workshop on Automated Verification of Infinite-State Systems (AVIS'04), Barcelona, Spain, 3rd-4th April 2004.
Abstract:
The automated verification of infinite-sate systems has made considerable progress these last ten years but is far from being yet a common practice. This might be that most available prototypes and tools are either:
- Manual (e.g. require end-users to provide manually a simple-enough model of the complex system), and/or
- User-unfriendly (e.g. require complex interactions with end-users), and/or
- Trivial (e.g. consider immediate essentially syntactic program properties) and/or
- Incorrect/unsound (e.g. do not explore the complete space of executions and so may forget about potential problems at run-time), and/or
- Inefficient (some may not terminate at all but by exhaustion of time/memory resources), and/or
- Imprecise (leading to too many false alarms that is spurious warnings on potential problems that can never occur at run-time).
We show that most of these problems arise from the use of inadequate abstractions (in the sense of the theory of abstract interpretation), in particular finitary abstractions aiming at reusing existing finite state exploration tools suffering from combinatorial explosion. By choosing appropriate infinitary, domain-aware, parametric and modular abstractions, one can design and implement automatic, sound, efficient and precise verifiers of complex properties of infinite-state systems. We provide the example of ASTRÉE, a static analyzer developed at the École normale supérieure (www.astree.ens.fr) that was able to prove completely automatically the absence of any run-time error in the primary flight control software of the Airbus A340 fly-by-wire system, a world première.
Slides of the 60mn presentation: The color transparencies are available as 1 slide per lanscape page for projection (1/1), 2 slides per portrait page for reading (2/1) and 4 slides per lanscape page for printing (4/1), in:
- PostScript: 1/1 .ps.gz, 2/1 .ps.gz, 4/1 .ps.gz for viewing with GhostScript and GhostView or (color) printing;
- PDF: 1/1 .pdf, 2/1 .pdf, 4/1 .pdf to be used with Acrobat Reader.

Bibliography:

\bibitem{Cousot-AVIS04}
P{.} Cousot.
\newblock Automated Verification of Infinite-State Systems by Abstract
Interpretation.
\newblock \emph{Third International Workshop on Automated Verification 
of Infinite-State Systems (AVIS'04)}, Barcelona, Spain, 3rd-4th April 2004.

@conference{Cousot-AVIS04,
   author =    {P{.} Cousot},
   title =     {Automated Verification of Infinite-State Systems by Abstract
                Interpretation},
   booktitle = {Third International Workshop on Automated Verification of 
                Infinite-State Systems (AVIS'04)},
   address =   {Barcelona, Spain},
   month =     {3rd-4th April},
   year =      2004,
}

copyright notice.
Last modified: Monday, 04-Jan-2010 13:41:21 CET