[klee-dev] Choice of SMT solver

2011-06-10 Thread Russell Wallace
On Tue, Jun 7, 2011 at 10:38 PM, Cristian Cadar c.cadar at imperial.ac.uk wrote: 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).

[klee-dev] Choice of SMT solver

2011-06-08 Thread Cristian Cadar
On 07/06/2011 23:40, Vijay Ganesh wrote: On Tue, Jun 7, 2011 at 5:38 PM, Cristian Cadar c.cadar at imperial.ac.uk mailto: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,

[klee-dev] Choice of SMT solver

2011-06-07 Thread Russell Wallace
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

[klee-dev] Choice of SMT solver

2011-06-07 Thread Vijay Ganesh
On Tue, Jun 7, 2011 at 5:38 PM, Cristian Cadar c.cadar at imperial.ac.ukwrote: 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