P. Cousot, The ASTRÉE analyzer

Patrick Cousot.
The ASTRÉE analyzer.
MIT/EECS/CSAIL Seminar, June 16^th, 2005.
Annonce: .pdf
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 (hundreds of thousands of 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 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-MintaMartin-05} P.~Cousot. \newblock The ASTR{\'E}E analyzer. \newblock MIT/EECS/CSAIL Seminar, Stata Center, June 16, 2005. @conference{Cousot-MIT-16-06-2005, author = {Patrick Cousot}, title = {The ASTR{\'E}E analyzer}, note = {MIT/EECS/CSAIL Seminar, Stata Center}, month = {16 \jun}, year = 2005, } copyright notice, Springer copyright Last modified: Monday, 07-May-2012 17:51:02 EDT