[klee-dev] KLEE-MultiSolver now available

Cristian Cadar c.cadar at imperial.ac.uk
Wed Oct 23 19:04:45 BST 2013


Thanks to Hristina Palikareva, our multi-solver extension to KLEE is now 
available as part of mainline KLEE.  The KLEE-MultiSolver extension is 
based on the metaSMT framework and is described in detail in our CAV'13 
paper (see 
http://srg.doc.ic.ac.uk/publications/klee-multisolver-cav-13.html).

While STP remains the default solver in KLEE, now you can also switch to 
Boolector or Z3 with a simple command-line flag (e.g., 
--use-metasmt=z3).  Adding additional metaSMT-compatible solvers should 
be quite easy.

To enable support for multiple solvers, you need to follow the 
instructions at http://srg.doc.ic.ac.uk/projects/klee-multisolver/. 
Please let us know if you run into any issues.

Cristian




More information about the klee-dev mailing list