Proceedings paper

Title:
PVAIR: Partial Variable Assignment InterpolatoR
Authors:
Pavel Jančík, Leonardo Alt, Grigory Fedyukovich, Antti E. J. Hyvärinen, Jan Kofroň, Natasha Sharygina
Publication:
Proceedings of FASE 2016
DOI:
Year:
2016
ISBN:
978-3-662-49665-7

Abstract:
Despite its recent popularity, program verification has to face practical limitations hindering its everyday use. One of these issues is scalability, both in terms of time and memory consumption. In this paper, we present Partial Variable Assignment InterpolatoR (PVAIR) – an interpolation tool exploiting partial variable assignments to significantly improve performance when computing several specialized Craig interpolants from a single proof. Subsequent interpolant processing during the verification process can thus be more efficient, improving scalability of the verification as such. We show with a wide range of experiments how our methods improve the interpolant computation in terms of their size. In particular, (i) we used benchmarks from the SAT competition and (ii) performed experiments in the domain of software upgrade checking.

BibTeX:
@inproceedings{jancik_pvair_2016,
    title = {{PVAIR: Partial Variable Assignment InterpolatoR}},
    author = {Jančík, Pavel and Alt, Leonardo and Fedyukovich, Grigory and Hyvärinen, Antti E. J. and Kofroň, Jan and Sharygina, Natasha},
    year = {2016},
    booktitle = {{Proceedings of FASE 2016}},
    editor = {Stevens, Perdita and Wąsowski, Andrzej},
    publisher = {Springer Berlin Heidelberg},
    series = {{Lecture Notes in Computer Science}},
    doi = {10.1007/978-3-662-49665-7_25},
    isbn = {978-3-662-49665-7},
    pages = {419--434},
    shorttitle = {PVAIR},
}