In TACAS’09.

In this talk, we will present the results reported in our CAV 2013 paper [6] on integrating support for multiple SMT solvers in the dynamic symbolic execution engine KLEE [2]. 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 (Boolector [1], STP [4] and Z3 [3]) through the metaSMT [5] 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