Formal Verification by Abstract Interpretation.

Patrick Cousot.
Formal Verification by Abstract Interpretation.
In Alwyn Goodloe and Suzette Person (Eds), 4th NASA Formal Methods Symposium (NFM 2012), Norfolk, Virginia, USA, April 3—5, 2012. Lecture Notes in Computer Science, vol. 7211, pp. 3—7, © Springer, 2012.
NFM 2012 paper (80 Kb)
Keywords: Abstract interpretation, Abstraction, Aerospace, Certification, Cyber-physical system, Formal Method, Mission-critical system, Runtime error, Safety-critical system, Scalability, Soundness, Static Analysis, Validation, Verification.
Abstract: Abstract interpretation is a theory of abstraction and constructive approximation of the mathematical structures used in the formal description of programming languages and the inference or verification of undecidable program properties. Developed in the late seventies with Radhia Cousot, it has since then been considerably applied to many aspects of programming, from syntax, to semantics, and proof methods where abstractions are sound and complete but incomputable to fully automatic, sound but incomplete approximate abstractions to solve undecidable problems such as static analysis of infinite state software systems, contract inference, type inference, termination inference, model-checking, abstraction refinement, program transformation (including watermarking), combination of decision procedures, security, malware detection, etc.
This last decade, abstract interpretation has been very successful in program verification for mission- and safety-critical systems. An example is Astrée (www.astree.ens.fr) which is a static analyzer to verify the absence of runtime errors in structured, very large C programs with complex memory usages, and involving complex boolean as well as floating-point computations (which are handled precisely and safely by taking all possible rounding errors into account), but without recursion or dynamic memory allocation. Astrée targets embedded applications as found in earth transportation, nuclear energy, medical instrumentation, aeronautics and space flight, in particular synchronous control/command such as electric flight control or more recently asynchronous systems as found in the automotive industry. Astrée is industrialized by AbsInt (www.absint.com/astree).

Slides of the 55mn presentation (.pdf)

\bibitem{Cousot-NFM2012}
Patrick Cousot.
\newblock Formal Verification by Abstract Interpretation.
\newblock In Alwyn Goodloe and Suzette Person, editors, \emph{4th NASA
Formal Methods Symposium (NFM 2012)}, Lecture Notes in Computer Science,
vol. 7226, pages 3--7, Springer-Verlag, Heidelberg, 2012.

@inproceedings{Cousot-NFM2012,
author = "Patrick Cousot",
title = "Formal Verification by Abstract Interpretation.",
booktitle = "4th NASA Formal Methods Symposium (NFM 2012)",
editor = "Alwyn Goodloe and Suzette Person",
series = "Lecture Notes in Computer Science",
publisher = "Springer-Verlag",
volume = "7226",
year = 2012,
pages = "3--7",
address = "Heidelberg"
}

copyright notice, Springer copyright notice
Last modified: Friday, 04-May-2012 10:01:26 EDT