Multi-solver Support in Symbolic Execution
File(s)klee-multisolver-cav-13.pdf (380.9 KB)
Accepted version
Author(s)
Palikareva, H
Cadar, C
Type
Conference Paper
Abstract
Abstract. One of the main challenges of dynamic symbolic execution—
an automated program analysis technique which has been successfully
employed to test a variety of software—is constraint solving. A key decision
in the design of a symbolic execution tool is the choice of a constraint
solver. While different solvers have different strengths, for most queries,
it is not possible to tell in advance which solver will perform better.
In this paper, we argue that symbolic execution tools can, and should,
make use of multiple constraint solvers. These solvers can be run competitively
in parallel, with the symbolic execution engine using the result
from the best-performing solver.
We present empirical data obtained by running the symbolic execution
engine KLEE on a set of real programs, and use it to highlight several important
characteristics of the constraint solving queries generated during
symbolic execution. In particular, we show the importance of constraint
caching and counterexample values on the (relative) performance of KLEE
configured to use different SMT solvers.
We have implemented multi-solver support in KLEE, using the metaSMT
framework, and explored how different state-of-the-art solvers compare
on a large set of constraint-solving queries. We also report on our ongoing
experience building a parallel portfolio solver in KLEE.
an automated program analysis technique which has been successfully
employed to test a variety of software—is constraint solving. A key decision
in the design of a symbolic execution tool is the choice of a constraint
solver. While different solvers have different strengths, for most queries,
it is not possible to tell in advance which solver will perform better.
In this paper, we argue that symbolic execution tools can, and should,
make use of multiple constraint solvers. These solvers can be run competitively
in parallel, with the symbolic execution engine using the result
from the best-performing solver.
We present empirical data obtained by running the symbolic execution
engine KLEE on a set of real programs, and use it to highlight several important
characteristics of the constraint solving queries generated during
symbolic execution. In particular, we show the importance of constraint
caching and counterexample values on the (relative) performance of KLEE
configured to use different SMT solvers.
We have implemented multi-solver support in KLEE, using the metaSMT
framework, and explored how different state-of-the-art solvers compare
on a large set of constraint-solving queries. We also report on our ongoing
experience building a parallel portfolio solver in KLEE.
Editor(s)
Sharygina, N
Veith, H
Date Issued
2013-07-13
Date Acceptance
2013-01-01
Citation
Computer Aided Verification 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013, Proceedings, 2013, pp.53-68
ISBN
978-3-642-39798-1
ISSN
0302-9743
Publisher
Springer
Start Page
53
End Page
68
Journal / Book Title
Computer Aided Verification 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013, Proceedings
Copyright Statement
The final publication is available at Springer via http://www.springer.com/us/book/9783642397981#aboutBook
Identifier
http://srg.doc.ic.ac.uk/publications/klee-multisolver-cav-13.html
Source
International Conference on Computer Aided Verification (CAV 2013)
Publication Status
Published
Start Date
2013-07-13
Finish Date
2013-07-19
Coverage Spatial
Saint Petersburg, Russian Federation