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). This being said, it would be great to try other constraint solvers too; some of them have also been used successfully for symbolic execution, and it would be useful to see how they'd work with KLEE. Most constraint solvers these days support the SMT-LIB format, (http://www.smtlib.org/), so the best thing would be to add support for SMT-LIB in KLEE. Let me know if you would like to pursue this project, I'd be happy to provide a few starting hints. > In particular, I notice some of the systems advertise the ability to > perform bit vector arithmetic, whereas others only advertise general > integer arithmetic. Is that a critical difference, or will a general > integer system more or less suffice? Yes, it is important to use arrays of bitvectors to represent symbolic memory objects. Not using a bit-level memory model could lead KLEE to explore infeasible paths and miss certain classes of bugs. Best, Cristian > (I asked a similar question at > http://stackoverflow.com/questions/6263962/smt-solvers-for-bit-vector-arithmetic > but no replies yet - obviously this is a somewhat specialized topic.) > _______________________________________________ > klee-dev mailing list > klee-dev at keeda.stanford.edu > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
