Hi, Thank you very much for your answer. Hercules sounds interesting. Is it open source?
I know KLEE produce an smt query. So, I think I could pass it to the z3 solver. But, I still not sure how the method get unsat core implementation in KLEE. For example in solver.cpp file there are methods like compute initial value and method to check the validity, so I would like to add get unsat core method in solver.cpp. Thank you. Sent from Samsung Mobile -------- Original message -------- From: Thuan Pham <[email protected]> Date: 22/09/2015 21:56 (GMT+08:00) To: felicia <[email protected]> Cc: [email protected] Subject: Re: [klee-dev] Metasmt using Z3 for getting unsat core Hi, I haven't tried to work with Z3 through metasmt. However, in our previous work (Hercules: reproducing crashes in real-world application binaries), I implemented an interface function for S2E (which is built on top of KLEE and QEMU) to get unsat-core from Z3. What I did is to formulate a SMT LIB-v2 query, save it to a file and invoke Z3 (as an external process) to get unsat-core (if the query is unsat). An example of the query is here http://rise4fun.com/Z3/smtc_core. If you want to get unsat-core from Z3 directly through metasmt interface, I think you just need to know the interface between KLEE and metasmt, formulate your query and send it through the interface. Hope it helps, Regards, Thuan On Tue, Sep 22, 2015 at 7:58 PM, felicia <[email protected]> wrote: Hi, I have installed metasmt and use Z3 as a solver. I actually need to implement code in KLEE where Z3 solver able to produce unsat-core. I am currently still not sure how I implement it in KLEE. I really appreciate if you can give suggestion about this. Thank you very much. Best Regards, Sent from Samsung Mobile _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
