An extension to KLEE that uses the metaSMT framework to add support for multiple SMT solvers (Boolector, STP and Z3), and its evaluation on 12 Coreutils applications.

Overview

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.

Download

See the instructions on how to configure, build and use the multi-solver extension of KLEE.

Research Support

This research project is generously sponsored by the UK EPSRC through the grant EP/J00636X/1.

Publications