K. Hoder,L. Kovacs, A. Voronkov:

"Playing in the grey area of proofs";

Talk: 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Philadelphia, US; 2012-01-22 - 2012-01-28; in: "Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)", J. Field, M. Hicks (ed.); ACM, (2012), ISBN: 978-1-4503-1083-3; 259 - 272.

Interpolation is an important technique in verification and static

analysis of programs. In particular, interpolants extracted from

proofs of various properties are used in invariant generation and

bounded model checking. A number of recent papers studies interpolation

in various theories and also extraction of smaller interpolants

from proofs. In particular, there are several algorithms

for extracting of interpolants from so-called local proofs. The main

contribution of this paper is a technique of minimising interpolants

based on transformations of what we call the "grey area" of local

proofs. Another contribution is a technique of transforming, under

certain common conditions, arbitrary proofs into local ones.

Unlike many other interpolation techniques, our technique is

very general and applies to arbitrary theories. Our approach is

implemented in the theorem prover Vampire and evaluated on a

large number of benchmarks coming from first-order theorem proving

and bounded model checking using logic with equality, uninterpreted

functions and linear integer arithmetic. Our experiments

demonstrate the power of the new techniques: for example, it is

not unusual that our proof transformation gives more than a tenfold

reduction in the size of interpolants.

Interpolation is an important technique in verification and static

analysis of programs. In particular, interpolants extracted from

proofs of various properties are used in invariant generation and

bounded model checking. A number of recent papers studies interpolation

in various theories and also extraction of smaller interpolants

from proofs. In particular, there are several algorithms

for extracting of interpolants from so-called local proofs. The main

contribution of this paper is a technique of minimising interpolants

based on transformations of what we call the "grey area" of local

proofs. Another contribution is a technique of transforming, under

certain common conditions, arbitrary proofs into local ones.

Unlike many other interpolation techniques, our technique is

very general and applies to arbitrary theories. Our approach is

implemented in the theorem prover Vampire and evaluated on a

large number of benchmarks coming from first-order theorem proving

and bounded model checking using logic with equality, uninterpreted

functions and linear integer arithmetic. Our experiments

demonstrate the power of the new techniques: for example, it is

not unusual that our proof transformation gives more than a tenfold

reduction in the size of interpolants.

Program verification, theorem proving, interpolation

http://dx.doi.org/10.1145/2103656.2103689

http://publik.tuwien.ac.at/files/PubDat_206750.pdf

Created from the Publication Database of the Vienna University of Technology.