Patrick Cousot, Abstracting Induction by Extrapolation and Interpolation

Patrick Cousot.
Abstracting Induction by Extrapolation and Interpolation
In Proceedings of the 16^th International Conference on Verification, Model Checking, and Abstract Interpretation, Deepak D'Souza, Akash Lal, and Kim Guldstrand Larsen (Eds), Mumbai, India, January 12—14, 2015. Lecture Notes in Computer Science, Vol. 8931, pp. 19—42, © Springer 2015.
Paper:
- Short version, 18 p., without proofs, PDF (1.7 MB)
- Long version, 24 p., with proofs, PDF (1.7 MB)
Slides of the 25mn presentation at VMCAI'2015:
- 4 slides per landscape page, (57.3 Mb)
Abstract:
We introduce a unified view of induction performed by automatic verification tools to prove a given program specification. This unification is done in the abstract interpretation framework using extrapolation (widening/dual-widening) and interpolation (narrowing, dual-narrowing, which are equivalent up to the exchange of the parameters). Dual-narrowing generalizes Craig interpolation in First Order Logic pre-ordered by implication to arbitrary abstract domains. An increasing iterative static analysis using extrapolation of successive iterates by widening followed by a decreasing iterative static analysis using interpolation of successive iterates by narrowing (both bounded by the specification) can be further improved by a increasing iterative static analysis using interpolation of iterates with the specification by dual-narrowing until reaching a fixpoint and checking whether it is inductive for the specification.
Keywords:
Abstract induction, Abstract interpretation, Dual-narrowing, Dual-widening, Extrapolation, Interpolation, Narrowing, Static analysis, Static checking, Static verification, Widening.

Bibliographic reference:

@inproceedings{DBLP:conf/vmcai/Cousot15,
  author    = {Patrick Cousot},
  title     = {Abstracting Induction by Extrapolation and Interpolation},
  booktitle = {Verification, Model Checking, and Abstract Interpretation - 16th International
               Conference, {VMCAI} 2015, Mumbai, India, January 12-14, 2015. Proceedings},
  pages     = {19--42},
  year      = {2015},
  crossref  = {DBLP:conf/vmcai/2015},
  url       = {http://dx.doi.org/10.1007/978-3-662-46081-8_2},
  doi       = {10.1007/978-3-662-46081-8_2},
}
@proceedings{DBLP:conf/vmcai/2015,
  editor    = {Deepak D'Souza and
               Akash Lal and
               Kim Guldstrand Larsen},
  title     = {Verification, Model Checking, and Abstract Interpretation - 16th International
               Conference, {VMCAI} 2015, Mumbai, India, January 12-14, 2015. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {8931},
  publisher = {Springer},
  year      = {2014},
  url       = {http://dx.doi.org/10.1007/978-3-662-46081-8},
  doi       = {10.1007/978-3-662-46081-8},
  isbn      = {978-3-662-46080-1},
}

copyright notice, Springer copyright notice
Last modified: Fri Oct 31 16:12:04 EDT 2014