PANDA: Simultaneous Predicate Abstraction and Concrete Execution

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F15%3A10311871" target="_blank" >RIV/00216208:11320/15:10311871 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/978-3-319-26287-1_6" target="_blank" >http://dx.doi.org/10.1007/978-3-319-26287-1_6</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-319-26287-1_6" target="_blank" >10.1007/978-3-319-26287-1_6</a>

Jazyk výsledku

angličtina

Název v původním jazyce

PANDA: Simultaneous Predicate Abstraction and Concrete Execution

Popis výsledku v původním jazyce

We present a new verification algorithm, PANDA, that combines predicate abstraction with concrete execution and dynamic analysis. Both the concrete and abstract state spaces of an input program are traversed simultaneously, guiding each other through on-the-fly mutual interaction. PANDA performs dynamic on-the-fly pruning of those branches in the abstract state space that diverge from the corresponding concrete trace. If the abstract branch is actually feasible for a different concrete trace, PANDA discovers the covering trace by exploring different data choices. Candidate spurious errors may also arise, for example, due to overapproximation of the points-to relation between heap objects. We eliminate all the spurious errors using the well-known approach based on lazy abstraction refinement with interpolants. Results of experiments with our prototype implementation show that PANDA can successfully verify programs that feature loops, recursion, and manipulation with objects and arrays.

Název v anglickém jazyce

PANDA: Simultaneous Predicate Abstraction and Concrete Execution

Popis výsledku anglicky

We present a new verification algorithm, PANDA, that combines predicate abstraction with concrete execution and dynamic analysis. Both the concrete and abstract state spaces of an input program are traversed simultaneously, guiding each other through on-the-fly mutual interaction. PANDA performs dynamic on-the-fly pruning of those branches in the abstract state space that diverge from the corresponding concrete trace. If the abstract branch is actually feasible for a different concrete trace, PANDA discovers the covering trace by exploring different data choices. Candidate spurious errors may also arise, for example, due to overapproximation of the points-to relation between heap objects. We eliminate all the spurious errors using the well-known approach based on lazy abstraction refinement with interpolants. Results of experiments with our prototype implementation show that PANDA can successfully verify programs that feature loops, recursion, and manipulation with objects and arrays.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

<a href="/cs/project/GP13-12121P" target="_blank" >GP13-12121P: Praktická verifikace programů s použitím kombinace statické a dynamické analýzy</a><br>

Návaznosti

S - Specificky vyzkum na vysokych skolach<br>I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2015

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

11th Haifa Verification Conference

ISBN

978-3-319-26286-4

ISSN

—

e-ISSN

—

Počet stran výsledku

17

Strana od-do

87-103

Název nakladatele

Springer

Místo vydání

Germany

Místo konání akce

Haifa, Israel

Datum konání akce

16. 11. 2015

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—