On 10/06/11 01:12, Russell Wallace wrote: > 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? Exactly -- in fact, there is already an option in KLEE to run STP as a separate process, which we often enable: --use-forked-stp.
Cristian
