z3 for klee

[K Kylin]

Hello,
I'm trying to make z3 into klee instead stp solver. with my mentor's
advice that z3 is more efficient. Maybe some work have been done by any of
you. If someone is doing this work, let me take part in, or if anyone
interest in it let's do it together.
thank you.

[Daniel Liew]

Hi,

To my knowledge this has already been done twice.

* By myself via SMTLIBv2 files ( see
https://github.com/delcypher/klee/tree/smtlib ). Invoking smtlib solvers
this way proved to be quite slow. This work allows any smtlibv2 solver that
supports the (get-value) command to be used by KLEE. STP itself can be used
this way too by using a small wrapper (stpwrap2). Z3 works without a
wrapper.

* By Hristina Palikareva using the meta-smt API. I'm not sure how much of
this work is published so I shall leave her to comment on this.

Regards,
Dan Liew

Post by K Kylin
Hello,
I'm trying to make z3 into klee instead stp solver. with my mentor's
advice that z3 is more efficient. Maybe some work have been done by any of
you. If someone is doing this work, let me take part in, or if anyone
interest in it let's do it together.
thank you.

[Hristina Palikareva]

Hi all,

We have recently developed a version of KLEE which supports Z3,
Boolector and STP. As Dan mentioned, we have used the metaSMT framework
(http://www.informatik.uni-bremen.de/agra/eng/metasmt.php), which
provides a unified API for using a number of SMT (and SAT) solvers
through their own API's. You can find some information about the project
here:

http://srg.doc.ic.ac.uk/projects/klee-multisolver/

We plan to start to slowly integrate the changes into mainline KLEE, but
if you'd like more information in the mean time, please drop me an email.

Best regards,
Hristina

Post by Daniel Liew
Hi,
To my knowledge this has already been done twice.
* By myself via SMTLIBv2 files ( see
https://github.com/delcypher/klee/tree/smtlib ). Invoking smtlib solvers
this way proved to be quite slow. This work allows any smtlibv2 solver
that supports the (get-value) command to be used by KLEE. STP itself can
be used this way too by using a small wrapper (stpwrap2). Z3 works
without a wrapper.
* By Hristina Palikareva using the meta-smt API. I'm not sure how much
of this work is published so I shall leave her to comment on this.
Regards,
Dan Liew
Hello,
I'm trying to make z3 into klee instead stp solver. with my
mentor's advice that z3 is more efficient. Maybe some work have been
done by any of you. If someone is doing this work, let me take part
in, or if anyone interest in it let's do it together.
thank you.