[klee-dev] Choice of SMT solver
hellovijay at gmail.com
Tue Jun 7 15:40:41 PDT 2011
On Tue, Jun 7, 2011 at 5:38 PM, Cristian Cadar <c.cadar at imperial.ac.uk>wrote:
> On 07/06/2011 12:12, Russell Wallace wrote:
> > I notice Klee chose STP for its SMT solver. I'm curious as to the
> > reason for this choice, and whether it would still be considered the
> > best today? The reason I ask is that I'm planning some experiments in
> > symbolic execution, and currently the list of potentially suitable
> > off-the-shelf solvers seems to be Beaver, Boolector, CVC3, OpenSMT,
> > Sateen, Sonolar, STP, Verit; which is a long list. I'm wondering how
> > to narrow it down.
> STP was initially developed in conjunction with KLEE's precursor, EXE,
> and has many optimizations that are useful for symbolic execution (see
> http://www.doc.ic.ac.uk/~cristic/papers/exe-ccs-06.pdf for details).
To this I would add that STP has been continuously improved over the years,
and it performs consistently better than other solvers for bit-vectors and
arrays (It won the SMTCOMP 2010 for bit-vectors).
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the klee-dev