Name
Abstract | ||
|---|---|---|
Symbolic execution, a standard technique in program analysis, is a particularly successful and popular component in systems for test-case generation. One of the open research problems is that the approach suffers from the path-explosion problem. We apply abstraction to symbolic execution, and refine the abstract model using counterexample-guided abstraction refinement (CEGAR), a standard technique from model checking. We also use refinement selection with existing and new heuristics to influence the behavior and further improve the performance of our refinement procedure. We implemented our new technique in the open-source software-verification framework CPACHEKARexperimental results show that the implementation is highly competitive. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1007/978-3-319-47166-2_14 | Lecture Notes in Computer Science |
Field | DocType | Volume |
Open research,Model checking,Abstraction,Programming language,Computer science,Heuristics,Symbolic execution,Abstraction refinement,Program analysis,CPAchecker | Conference | 9952 |
ISSN | Citations | PageRank |
0302-9743 | 6 | 0.42 |
References | Authors | |
17 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Dirk Beyer | 1 | 1736 | 100.85 |
| Thomas Lemberger | 2 | 17 | 3.59 |