[Zurück]


Vorträge und Posterpräsentationen (mit Tagungsband-Eintrag):

K. Hoder, L. Kovacs, A. Voronkov:
"Playing in the grey area of proofs";
Vortrag: 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Philadelphia, US; 22.01.2012 - 28.01.2012; in: "Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)", J. Field, M. Hicks (Hrg.); ACM, (2012), ISBN: 978-1-4503-1083-3; S. 259 - 272.



Kurzfassung deutsch:
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.

Kurzfassung englisch:
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.

Schlagworte:
Program verification, theorem proving, interpolation


"Offizielle" elektronische Version der Publikation (entsprechend ihrem Digital Object Identifier - DOI)
http://dx.doi.org/10.1145/2103656.2103689

Elektronische Version der Publikation:
http://publik.tuwien.ac.at/files/PubDat_206750.pdf


Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.