PVAIR: Partial Variable Assignment InterpolatoR
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F16%3A10315954" target="_blank" >RIV/00216208:11320/16:10315954 - isvavai.cz</a>
Result on the web
<a href="http://dx.doi.org/10.1007/978-3-662-49665-7_25" target="_blank" >http://dx.doi.org/10.1007/978-3-662-49665-7_25</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-662-49665-7_25" target="_blank" >10.1007/978-3-662-49665-7_25</a>
Alternative languages
Result language
angličtina
Original language name
PVAIR: Partial Variable Assignment InterpolatoR
Original language description
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.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
IN - Informatics
OECD FORD branch
—
Result continuities
Project
<a href="/en/project/GA14-11384S" target="_blank" >GA14-11384S: Automatic Formal Analysis and Verification of Programs with Complex Unbounded Data and Control Structures</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2016
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Fundamental Approaches to Software Engineering: 19th International Conference, FASE 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2--8, 2016, Proceedings
ISBN
978-3-662-49664-0
ISSN
0302-9743
e-ISSN
—
Number of pages
16
Pages from-to
419-434
Publisher name
Springer Berlin Heidelberg
Place of publication
Berlin
Event location
Eindhoven, Nizozemí
Event date
Apr 2, 2016
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—