Paper Info
Title
CPA-SymExec: efficient symbolic execution in CPAchecker.
Abstract
We present CPA-SymExec, a tool for symbolic execution that is implemented in the open-source, configurable verification framework CPAchecker. Our implementation automatically detects which symbolic facts to track, in order to obtain a small set of constraints that are necessary to decide reachability of a program area of interest. CPA-SymExec is based on abstraction and counterexample-guided abstraction refinement (CEGAR), and uses a constraint-interpolation approach to detect symbolic facts. We show that our implementation can better mitigate the path-explosion problem than symbolic execution without abstraction, by comparing the performance to the state-of-the-art Klee-based symbolic-execution engine Symbiotic and to Klee itself. For the experiments we use two kinds of analysis tasks: one for finding an executable path to a specific location of interest (e.g., if a test vector is desired to show that a certain behavior occurs), and one for confirming that no executable path to a specific location exists (e.g., if it is desired to show that a certain behavior never occurs). CPA-SymExec is released under the Apache 2 license and available (inclusive source code) at <a href="https://cpachecker.sosy-lab.org">https://cpachecker.sosy-lab.org</a>. A demonstration video is available at <a href="https://youtu.be/qoBHtvPKtnw">https://youtu.be/qoBHtvPKtnw</a>.
Year
DOI
Venue
2018
10.1145/3238147.3240478
ASE
Keywords
Field
DocType
Symbolic Execution, Program Analysis, Test-Case Generation
Test vector,Abstraction,Source code,Computer science,Theoretical computer science,Reachability,Symbolic execution,Program analysis,CPAchecker,Executable
Conference
ISSN
ISBN
Citations 
1527-1366
978-1-4503-5937-5
1
PageRank 
References 
Authors
0.37
17
2
Name
Order
Citations
PageRank
Dirk Beyer11736100.85
Thomas Lemberger2173.59