Leveraging Interpolant Strength in Model Checking

Result code in 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>

Result on the web

<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>

Result language

angličtina

Original language name

Leveraging Interpolant Strength in Model Checking

Original language description

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

Czech name

—

Czech description

—

Type

J_x - Unclassified - Peer-reviewed scientific article (Jimp, Jsc and Jost)

CEP classification

JC - Computer hardware and software

OECD FORD branch

—

Project

<a href="/en/project/GPP202%2F12%2FP180" target="_blank" >GPP202/12/P180: Model checking concurrent software using automated deduction of object ownership patterns</a><br>

Continuities

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

Publication year

2012

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Name of the periodical

Lecture Notes in Computer Science

ISSN

0302-9743

e-ISSN

—

Volume of the periodical

2012

Issue of the periodical within the volume

7358

Country of publishing house

DE - GERMANY

Number of pages

15

Pages from-to

193-209

UT code for WoS article

—

EID of the result in the Scopus database

—