Leveraging Interpolant Strength in Model Checking

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F12%3A10124355" target="_blank" >RIV/00216208:11320/12:10124355 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/978-3-642-31424-7_18" target="_blank" >http://dx.doi.org/10.1007/978-3-642-31424-7_18</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-642-31424-7_18" target="_blank" >10.1007/978-3-642-31424-7_18</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Leveraging Interpolant Strength in Model Checking

Popis výsledku v původním jazyce

Craig interpolation is a well known method of abstraction successfully used in both hardware and software model checking. The logical strength of interpolants can affect the quality of approximations and consequently the performance of the model checkers. Recently, it was observed that for the same resolution proof a complete lattice of interpolants ordered by strength can be derived. Most state-of-the-art model checking techniques based on interpolation subject the interpolants to constraints that ensure efficient verification as, for example, in transition relation approximation for bounded model checking, counterexample-guided abstraction refinement and function summarization for software update checking. However, in general, these verification-specific constraints are not satisfied by all possible interpolants. The paper analyzes the restrictions within the lattice of interpolants under which the required constraints are satisfied. This enables investigation of the effect of the st

Název v anglickém jazyce

Leveraging Interpolant Strength in Model Checking

Popis výsledku anglicky

Craig interpolation is a well known method of abstraction successfully used in both hardware and software model checking. The logical strength of interpolants can affect the quality of approximations and consequently the performance of the model checkers. Recently, it was observed that for the same resolution proof a complete lattice of interpolants ordered by strength can be derived. Most state-of-the-art model checking techniques based on interpolation subject the interpolants to constraints that ensure efficient verification as, for example, in transition relation approximation for bounded model checking, counterexample-guided abstraction refinement and function summarization for software update checking. However, in general, these verification-specific constraints are not satisfied by all possible interpolants. The paper analyzes the restrictions within the lattice of interpolants under which the required constraints are satisfied. This enables investigation of the effect of the st

Druh

J_x - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)

CEP obor

JC - Počítačový hardware a software

OECD FORD obor

—

Projekt

<a href="/cs/project/GPP202%2F12%2FP180" target="_blank" >GPP202/12/P180: Model checking paralelního software s využitím automatické dedukce object ownership vzorů</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2012

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ů

Název periodika

Lecture Notes in Computer Science

ISSN

0302-9743

e-ISSN

—

Svazek periodika

2012

Číslo periodika v rámci svazku

7358

Stát vydavatele periodika

DE - Spolková republika Německo

Počet stran výsledku

15

Strana od-do

193-209

Kód UT WoS článku

—

EID výsledku v databázi Scopus

—