P. Cousot, Verification of Large Complex Software by Abstract Interpretation

Patrick Cousot.
Verification of Large Complex Software by Abstract Interpretation.
11th Annual Asian Computing Science Conference, ASIAN'06, National Center of Sciences, Tokyo, Japan, 6—8 December 2006.
Abstract:
     Since almost any large complex software has bugs which are not found by test methods, researchers have developed program correctness proof methods which have been successful in the small. This consists in defining a semantics formally describing the executions of a program and then in proving a theorem stating that these executions have a given property (for example that an expected result is provided in a finite time). Fundamental mathematical undecidability results show that these proofs cannot be done automatically by computers.
     Confronted with this fundamental difficulty, abstract interpretation proceeds by correct approximation of the semantics. If the approximation is sound, no potential error can ever be overlooked, a basic requirement of formal verification methods. If the approximation is coarse enough, it is computable. If it is precise enough, it yields a correctness proof. The goal is therefore to find cheap approximations (so as to scale up in the large) which are precise enough (to avoid false alarms where a property does hold but this cannot be proved because of an approximation which is too imprecise).
     We will introduce a few elements of abstract interpretation and explain how to formalize the abstraction of semantic properties so as to obtain computable approximations leading to effective algorithms for the static analysis of the possible behaviors of programs.
     Finally, we will describe an example of application of the theory to the proof of absence of runtime errors on synchronous control/command and underly the difficulties (such as floating point computations). This approach was applied with success to the verification of the electric flight control of commercial planes.

keywords:
Abstract interpretation,Semantics, Abstraction, Approximation, Static Analysis, Run time errors.
Slides of the 90 mn 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.

Bibliographic reference:

\bibitem{Cousot-ASIAN06}
P.~Cousot.
\newblock Verification of Large Complex Software by Abstract Interpretation.
\newblock \emph{11th Annual Asian Computing Science Conference, ASIAN'06}, 
         National Center of Sciences, Tokyo, Japan, 6--8 December 2006.

@conference{Cousot-ASIAN06,
   author =    {P{.} Cousot},
   title =     {Verification of Large Complex Software by Abstract Interpretation},
   note    =   {\emph{11th Annual Asian Computing Science Conference, ASIAN'06}, 
                National Center of Sciences, Tokyo, Japan},
   month =     {6--8 December},
   year =      2006,
}

copyright notice
Last modified: Monday, 04-Jan-2010 13:40:42 CET