@inproceedings{c95abd1a3eba4eeea082f485c67d4530,
title = "Abstracting induction by extrapolation and interpolation",
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",
author = "Patrick Cousot",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 2015.; 16th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2015 ; Conference date: 12-01-2015 Through 14-01-2015",
year = "2015",
doi = "10.1007/978-3-662-46081-8_2",
language = "English (US)",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "19--42",
editor = "Deepak D{\textquoteright}Souza and Akash Lal and Larsen, {Kim Guldstrand}",
booktitle = "Verification, Model Checking and Abstract Interpretation - 16th International Conference, VMCAI 2015, Proceedings",
}