P. Cousot, Static Verification of Safety Critical Code by Abstract Interpretation

Patrick Cousot.
Static Verification of Safety Critical Code by Abstract Interpretation.
Distinguished Lecturer Series, Department of Computing and Information Sciences , Kansas State University, Manhattan, Kansas, USA, September 5th, 2006.
Abstract:
The talk briefly reviews abstract interpretation and its main applications. It then presents a practical application of abstract interpretation to the verification of safety critical embedded control-command software by the ASTRÉE static analyzer. It has been applied with success to the verification of absence of runtime errors in the control part of the primary flight control software of fly-by-wire systems of commercial planes. The state space of such huge programs (up to a million lines) is so large that it cannot be explored explicitly by model-checking nor reasonably covered by testing. A (computer-aided) formal proof would be humanely insurmountable and economically very costly. The key to the verification by static analysis is the appropriate experimental choice of abstractions which can be tuned to yield no false alarm, certainly a world première for a program of that size (see the ASTRÉE project, http://www.astree.ens.fr/). We will conclude by grand challenges for static program/specification analysis in the next 5 to 10 years.
Keywords:
Abstract Interpretation, Static Analysis, Embedded Systems, Control/Command Software, Reachability, Runtime Error, Verification.
Slides of the 90 mn presentation: .pdf.

Bibliographic reference:

\bibitem{Cousot-Kstate-06-09-05}
P.~Cousot.
\newblock Static Verification of Safety Critical Code by Abstract 
          Interpretation.
\newblock \emph{Distinguished Lecturer Series,  Computing and 
          Information Sciences, Kansas State University}, 
          Manhattan, Kansas, USA, September 5th, 2006.

@conference{Cousot-Kstate-06-09-05,
   author =    {P{.} Cousot},
   title =     {Static Verification of Safety Critical Code by Abstract 
                Interpretation},
   note    =   {\emph{Distinguished Lecturer Series,  Computing and 
                Information Sciences,  Kansas State University}, 
                Manhattan, Kansas, USA},
   month =     {September 5th},
   year =      2006,
}

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