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). 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.
Right, yeah, that makes sense, thanks. > Most constraint solvers these days support the SMT-LIB format, > (http://www.smtlib.org/) True. That would mean running the solver as a separate process, but the overhead of that is probably small compared to the computational effort of solving nontrivial constraint problems, and it also has the advantage, I imagine, of insulating the original process in case the solver does something like hitting stack overflow?
