P. Cousot, Static Software Analysis, in the Large

Patrick Cousot.
Static Software Analysis, in the Large.
Max Planck Institute for Software Systems, Distinguished Lecture Series, August 26, 2008, Saarbrücken, Building MPI-SWS Saarbrücken, Room 019 (simultaneous videocast at Kaiserslautern, Building MPI-SWS Kaiserslautern, Room 206).
Abstract of the 60 mn talk :
Static software analysis has known brilliant successes in the small, by proving complex program properties of programs of a few dozen or hundreds of lines, either by systematic exploration of the state space or by interactive deductive methods. To scale up is a definite problem. Very few static analyzers are able to scale up to millions of lines without sacrificing soundness and/or precision. Unsound static analysis may be useful for bug finding but is less useless in safety critical applications where the absence of bugs, at least of some categories of common bugs, should be formally verified.
After recalling the basic principles of abstract interpretation including the notions of abstraction, approximation, soundness, completeness, false alarm, etc., we introduce the domain-specific static analyzer ASTRÉE (www.astree.ens.fr) for proving the absence of runtime errors in safety critical real time embedded synchronous software in the large.
The talk emphasizes soundness (no runtime error is ever omitted), parametrization (the ability to refine abstractions by options and analysis directives), extensibility (the easy incorporation of new abstractions to refine the approximation), precision (few or no false alarms for programs in the considered application domain) and scalability (the analyzer scales to millions of lines).
In conclusion, present-day software engineering methodology, which is based on the control of the design, coding and testing processes should evolve in the near future, to incorporate a systematic control of final software product thanks to domain-specific analyzers that scale up.
Slides:
- 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.

Bibliographic reference:

\bibitem{Cousot08-FICS}
P. Cousot.
\newblock Static Software Analysis, in the Large.
\newblock Max Planck Institute for Software Systems, Distinguished Lecture 
          Series, Saar{b\r"u}cken, Germany, August 26, 2008.

@unpublished{Cousot08-FICS,
   author =    {P{.} Cousot},
   title =     {Static Software Analysis, in the Large},
   note =      {Max Planck Institute for Software Systems, 
                Distinguished Lecture Series, Saar{b\r"u}cken, 
                Germany},
   month =     26 # aug,
   year =      2008,
}

copyright notice
Last modified: Thursday, 04-Oct-2007 15:57:05 CEST