On Interpolants and Variable Assignments
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F14%3A10281323" target="_blank" >RIV/00216208:11320/14:10281323 - isvavai.cz</a>
Výsledek na webu
<a href="http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD14/proceedings/22_jancik.pdf" target="_blank" >http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD14/proceedings/22_jancik.pdf</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1109/FMCAD.2014.6987604" target="_blank" >10.1109/FMCAD.2014.6987604</a>
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
On Interpolants and Variable Assignments
Popis výsledku v původním jazyce
Craig interpolants are widely used in program verification as a means of abstraction. In this paper, we (i) introduce Partial Variable Assignment Interpolants (PVAIs) as a generalization of Craig interpolants. A variable assignment focuses computed interpolants by restricting the set of clauses taken into account during interpolation. PVAIs can be for example employed in the context of DAG interpolation, in order to prevent unwanted out-of-scope variables to appear in interpolants. Furthermore, we (ii)present a way to compute PVAIs for propositional logic based on an extension of the Labeled Interpolation Systems, and (iii) analyze the strength of computed interpolants and prove the conditions under which they have the path interpolation property.
Název v anglickém jazyce
On Interpolants and Variable Assignments
Popis výsledku anglicky
Craig interpolants are widely used in program verification as a means of abstraction. In this paper, we (i) introduce Partial Variable Assignment Interpolants (PVAIs) as a generalization of Craig interpolants. A variable assignment focuses computed interpolants by restricting the set of clauses taken into account during interpolation. PVAIs can be for example employed in the context of DAG interpolation, in order to prevent unwanted out-of-scope variables to appear in interpolants. Furthermore, we (ii)present a way to compute PVAIs for propositional logic based on an extension of the Labeled Interpolation Systems, and (iii) analyze the strength of computed interpolants and prove the conditions under which they have the path interpolation property.
Klasifikace
Druh
D - Stať ve sborníku
CEP obor
IN - Informatika
OECD FORD obor
—
Návaznosti výsledku
Projekt
<a href="/cs/project/GA14-11384S" target="_blank" >GA14-11384S: Automatizovaná formální analýza a verifikace programů se složitými datovými a řídicími strukturami s předem neomezenou velikostí</a><br>
Návaznosti
S - Specificky vyzkum na vysokych skolach
Ostatní
Rok uplatnění
2014
Kód důvěrnosti údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Údaje specifické pro druh výsledku
Název statě ve sborníku
Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design (FMCAD 2014)
ISBN
978-0-9835678-4-4
ISSN
—
e-ISSN
—
Počet stran výsledku
8
Strana od-do
123-130
Název nakladatele
Neuveden
Místo vydání
Lausanne, Švýcarsko
Místo konání akce
Lausanne
Datum konání akce
21. 10. 2014
Typ akce podle státní příslušnosti
WRD - Celosvětová akce
Kód UT WoS článku
—