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). -Vijay. -------------- next part -------------- An HTML attachment was scrubbed... URL: http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20110607/6cfc5f9f/attachment.html
