Exploiting partial variable assignment in interpolation-based model checking
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F19%3A10404095" target="_blank" >RIV/00216208:11320/19:10404095 - isvavai.cz</a>
Výsledek na webu
<a href="https://verso.is.cuni.cz/pub/verso.fpl?fname=obd_publikace_handle&handle=FaeSePhppP" target="_blank" >https://verso.is.cuni.cz/pub/verso.fpl?fname=obd_publikace_handle&handle=FaeSePhppP</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/s10703-019-00342-z" target="_blank" >10.1007/s10703-019-00342-z</a>
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
Exploiting partial variable assignment in interpolation-based model checking
Popis výsledku v původním jazyce
Craig interpolation has been successfully employed in symbolic program verification as a means of abstraction for sets of program states. In this article, we present the partial variable assignment interpolation system, an extension of the labeled interpolation system, enriched by partial variable assignments. It allows for both generation of smaller interpolants as well as for their faster computation. We present proofs of important properties of the interpolation system as well as a set of experiments proving its usefulness.
Název v anglickém jazyce
Exploiting partial variable assignment in interpolation-based model checking
Popis výsledku anglicky
Craig interpolation has been successfully employed in symbolic program verification as a means of abstraction for sets of program states. In this article, we present the partial variable assignment interpolation system, an extension of the labeled interpolation system, enriched by partial variable assignments. It allows for both generation of smaller interpolants as well as for their faster computation. We present proofs of important properties of the interpolation system as well as a set of experiments proving its usefulness.
Klasifikace
Druh
J<sub>imp</sub> - Článek v periodiku v databázi Web of Science
CEP obor
—
OECD FORD obor
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Návaznosti výsledku
Projekt
<a href="/cs/project/GA18-17403S" target="_blank" >GA18-17403S: Automatická inkrementální verifikace a odstraňování chyb pro souběžné systémy</a><br>
Návaznosti
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Ostatní
Rok uplatnění
2019
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 periodika
Formal Methods in System Design
ISSN
0925-9856
e-ISSN
—
Svazek periodika
55
Číslo periodika v rámci svazku
December 2019
Stát vydavatele periodika
US - Spojené státy americké
Počet stran výsledku
39
Strana od-do
33-71
Kód UT WoS článku
000495056000001
EID výsledku v databázi Scopus
2-s2.0-85074833229