On Interpolants and Variable Assignments

Kód výsledku v IS VaVaI

RIV/00216208:11320/14:10281323 - isvavai.cz

Výsledek na webu

http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD14/proceedings/22_jancik.pdf

DOI - Digital Object Identifier

10.1109/FMCAD.2014.6987604

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.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

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í

Návaznosti

S - Specificky vyzkum na vysokych skolach

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ů

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

—