P. Cousot, Application of Abstract Interpretation to the Static Verification of Safety Critical Code

Patrick Cousot.
Application of Abstract Interpretation to the Static Verification of Safety Critical Code.
Seminar, IBM Thomas J. Watson Research Center, Hawthorne, New York, USA, January 20th, 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\'EE 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\`ere 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-IBM-01-06-05}
P.~Cousot.
\newblock Application of Abstract Interpretation to the Static 
          Verification of Safety Critical Code.
\newblock \emph{Seminar, IBM Thomas J. Watson Research Center}, 
          Hawthorne, New York, USA, January 20th, 2006.

@conference{Cousot-IBM-01-06-05,
   author =    {P{.} Cousot},
   title =     {Application of Abstract Interpretation to the Static 
                Verification of Safety Critical Code},
   note    =   {\emph{Seminar, IBM Thomas J. Watson Research Center}, 
                Hawthorne, New York, USA, January 20th, 2006},
   month =     {20 January},
   year =      2006,
}

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