P. Cousot, Abstract Interpretation-based Formal Verification of Complex Computer Systems

Patrick Cousot.
Abstract Interpretation-based Formal Verification of Complex Computer Systems.
Minta Martin Lecture, Department of Aeronautics and Astronautics, Bartos Theater, MIT, Friday May 13^th, 2005.
Annonce: .pdf
Abstract:
   The computing power of computers, which has doubled every eighteen months since 1975, is now so huge that it is possible to embed very large and extremely sophisticated software in ever more complex systems, from small devices to large-scale, interconnected, distributed, real-time systems. This includes the most highly mission-critical and safetycritical computer-based infrastructures, as produced by the aerospace, automotive, customer electronics, defense, energy, industrial automation, medical device, rail transportation and telecommunication industries.
   The exponential expansion of software in all application domains leads to the unfortunate situation where software engineers can build increasingly large software, but are less and less confident in the quality of the software they produce. Defaults in such complex software are not so uncommon, as can be experienced everyday by computer end-users. Such bugs can have catastrophic consequences as the most famous, and certainly most costly one, to date, the overflow at the origin of the failure of the Ariane 5.01 flight on 4 June 1996.
   Because present-day software engineering, which is almost exclusively manual, with very few useful automated tools does not scale up, a grand challenge is therefore to develop knowledge, methods, technologies and tools to master software complexity.
   Mathematical results show that the automatic software verification problem is indeed extremely hard.
   Recent progress in the rigorous analysis of software and embedded systems has been possible thanks to abstract interpretation, formalizing the idea of sound approximation of complex mathematical structures, in particular those involved in the semantic models of computer systems. Abstract interpretation can be applied to the systematic construction of methods and effective algorithms to approximate undecidable or very complex problems in computer science such that the semantics, the proof, the static analysis, the verification, the safety and security of software and hardware computer systems.
   Abstract interpretation-based static analysis, which automatically infers dynamic properties of computer systems, has been very successfully applied in recent years to automatically verify complex properties of real-time, safety critical, embedded systems, such as the verification of absence of runtime errors in the primary flight control software of commercial airplanes.
Keywords:
Abstract Interpretation, Static Analysis, Embedded Systems, Control/Command Software, Reachability, Runtime Error, Verification.
Slides of the 60 mn presentation: .pdf

Bibliographic reference:

\bibitem{Cousot-MintaMartin-05}
P.~Cousot.
\newblock Abstract Interpretation-based Formal Verification of 
          Complex Computer Systems.
\newblock Minta Martin Lecture, Department of Aeronautics and 
          Astronautics, Massachusetts Institute of Technology, 
          May 13, 2005.

@conference{Cousot-MintaMartin-05,
   author =    {P{.} Cousot},
   title =     {Abstract Interpretation-based Formal 
                Verification of Complex Computer Systems},
   address =   {Minta Martin Lecture, Department of Aeronautics and 
                Astronautics, Massachusetts Institute of Technology},
   month =     {13 May},
   year =      2005,
}

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