zbMATH — the first resource for mathematics

Interpolants and symbolic model checking. (English) Zbl 1132.68474
Cook, Byron (ed.) et al., Verification, model checking, and abstract interpretation. 8th international conference, VMCAI 2007, Nice, France, January 14–16, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-69735-0/pbk). Lecture Notes in Computer Science 4349, 89-90 (2007).
Summary: An interpolant for a mutually inconsistent pair of formulas \((A,B)\) is a formula that is (1) implied by \(A\), (2) inconsistent with \(B\), and (3) expressed over the common variables of \(A\) and \(B\). An interpolant can be efficiently derived from a refutation of \(A \land B\), for certain theories and proof systems. In this tutorial we will cover methods of generating interpolants, and applications of interpolants, including invariant generation and abstraction refinement.
For the entire collection see [Zbl 1131.68006].

68Q60 Specification and verification (program logics, model checking, etc.)
PDF BibTeX Cite
Full Text: DOI