P. Cousot & R. Cousot, Abstract interpretation and a range of applications

Patrick Cousot and Radhia Cousot.
Abstract interpretation and a range of applications.
Seminario del Dipartimento di Informatica, Università Ca' Foscari Venezia, Mestre, Italy. October 23^rd, 2006.
Abstract:
     Since almost any complex software has bugs, researchers have developed program correctness proof methods. 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 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 coarse enough, it is computable. If it is precise enough, it yields a correctness proof. The goal is therefore to find cheap approximations which are precise enough.
     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 behaviours 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 avionic software.
Keywords:
Abstract Interpretation, Semantics, Static analysis, Embedded real-time safety critical software.
Slides of the 55 mn presentation: .pdf

Bibliographic reference:

\bibitem{CousotCousot-Mestre-23-10-06}
P.~Cousot \& R.~Cousot.
\newblock Abstract interpretation and a range of applications.
\newblock \emph{Seminario del Dipartimento di Informatica}, 
         Universit\`a Ca' Foscari Venezia, Mestre, Italy, October 23${^\mathrm{rd}}$ 2006.

@inProceedings{CousotCousot-Mestre-23-10-06,
   author =    {P{.} Cousot and R{.} Cousot},
   title =     {Abstract interpretation and a range of applications},
   booktitle = {Seminario del Dipartimento di Informatica},
   address =   {Universit\`a Ca' Foscari Venezia, Mestre, Italy},
   month =     {October 23${^\mathrm{rd}}$},
   year =      2006,
}

copyright notice
Last modified: Monday, 07-May-2012 17:51:04 EDT