PANDA: Simultaneous Predicate Abstraction and Concrete Execution
The result's identifiers
Result code in 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>
Result on the web
<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>
Alternative languages
Result language
angličtina
Original language name
PANDA: Simultaneous Predicate Abstraction and Concrete Execution
Original language description
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.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
IN - Informatics
OECD FORD branch
—
Result continuities
Project
<a href="/en/project/GP13-12121P" target="_blank" >GP13-12121P: Practical Program Verification Using Combination of Static and Dynamic Analysis</a><br>
Continuities
S - Specificky vyzkum na vysokych skolach<br>I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace
Others
Publication year
2015
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
11th Haifa Verification Conference
ISBN
978-3-319-26286-4
ISSN
—
e-ISSN
—
Number of pages
17
Pages from-to
87-103
Publisher name
Springer
Place of publication
Germany
Event location
Haifa, Israel
Event date
Nov 16, 2015
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—