[klee-dev] Mockup of klee-like tool using integer and real non-linear logics

[Pablo González de Aledo]

Hi there. Following

http://mailman.ic.ac.uk/pipermail/klee-dev/2013-April/000145.html

I've been working last months in a tool similar to klee, but using integer
and real datatypes instead of bitvectors. I use Microsoft Z3 solver instead
of STP, which allows me to solve non-linearly constrained problems with
AUFNIRA logic.

The main advantages of this approach are:

* It can search paths in which float variables are involved.
* It can search paths which involves non-linear constraints.(
multiplication and division included )
* The complexity of solving problems does not scale with the number of
bits, but with the number of variables.
* Using the jsmtlib interface, it's easy to test different solvers and
different logics to evaluate their performance.

The main disadvantage right now is that, abstracting datatypes this way
complicates the handling of bitwise operators like &, |, ~,^ ... And of
course the fact that it's only a mockup and can not cope with real
industrial examples.

Nevertheless, I've put a copy of the code in
https://github.com/pablo-aledo/forest hoping that someone could give me his
opinion. Do you think this could be an interesting path to follow?.

Thanks.
-------------- next part --------------
HTML attachment scrubbed and removed