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).
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,
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
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