Patrick Cousot, Verification by Abstract Interpretation, Soundness and Abstract Induction

Patrick Cousot.
Verification by Abstract Interpretation, Soundness and Abstract Induction
In Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming (PPDP 2015), Siena, Italy, July 14-16, 2015, Elvira Albert and Moreno Falaschi (Eds), © ACM SIGPLAN, 2015.
Paper:
- PDF (2.2 MB)
Slides of the 60mn presentation at PPDP'2015:
- 4 slides per landscape page, (10 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, Induction, Interpolation, Mathematical induction, Narrowing, Semantics, Soundness, Static analysis, Static checking, Static verification, Undecidability, Verification, Widening.

Bibliographic reference:

\bibitem{PCousot-PPDP-15}
P.~Cousot.
\newblock Verification by Abstract Interpretation, Soundness and Abstract Induction.
\newblock In \emph{Proceedings of the 17th International Symposium on Principles and 
   Practice of Declarative Programming (PPDP 2015)}, Siena, Italy, July 14-16, 2015, 
   Elvira Albert and Moreno Falaschi (Eds), \textcopy~ACM SIGPLAN, 2015.

copyright notice, ACM Author Rights and Publishing Policy
Last modified: Fri Sep 18 08:28:54 EDT 2015