Multi-solver Support in Symbolic Execution

ABSTRACT. In this talk, we will present the results reported in our CAV 2013 paper on integrating support for multiple SMT solvers in the dynamic symbolic execution engine KLEE. In particular, we will outline the key characteristics of the SMT queries generated during symbolic execution, introduce an extension of KLEE that uses a number of state-of-the-art SMT solvers (Z3, Boolector and STP) through the metaSMT solver framework, and compare the solvers' performance when run on large sets of QF_ABV queries obtained during the symbolic execution of real-world software. In addition, we will discuss several options for designing a parallel portfolio solver for symbolic execution tools.