Patrick Cousot, Sound Verification by Abstract Interpretation

Patrick Cousot.
Sound Verification by Abstract Interpretation
In Proceedings of the The Sixth Workshop on Tools for Automatic Program Analysis, Josh Berdine (Ed), Saint-Malo, France 8 September 2015.
Slides of the 60mn presentation at TAPAS'2015:
- 4 slides per landscape page, (1.9 Mb)
Abstract:
Automatic program verification tools have to cope with programming language and machine semantics, undecidability, and mathematical induction, and so are all complex and imperfect. The ins and outs of automatic program verification will be discussed in light of the theory and practice of abstract interpretation.
Keywords:
Abstract induction, Abstract interpretation, Abstraction, Completeness, Dual-narrowing, Dual-widening, Extrapolation, Formal methods, Galois Connection, Interpolation, Narrowing, Semantics, Soundness, Static analysis, Static checking, Static verification, Verification, Widening.

Bibliographic reference:

\bibitem{PCousot-TAPAS-15}
P.~Cousot.
\newblock Sound Verification by Abstract Interpretation.
\newblock In \emph{The Sixth Workshop on Tools for Automatic Program Analysis},
           8 September 2015, Saint-Malo, France.

copyright notice,
Last modified: Thu Sep 17 17:51:06 EDT 2015