[klee-dev] Current status of Z3 with FP-support

[Dan Liew]

Hi,

On 12 June 2017 at 13:12, Henrik Tjäder <henrik at tjaders.com> wrote:
> Hi,
>
> Reading (1) and quoting Dan Liew,
>
> "I'm aware of klee-fp. However I should warn you (so that you don't
> waste time doing this) that I (and another research institution) have
> already extended KLEE with floating point support using Z3. We intend
> to open source our implementations in the very near future."
>
> I am curious about the state of this ongoing work, and if there are any
> need for testers or such.

The implementation that we have currently will be open sourced once we
have some published work using it.

However it is our intention to upstream this work to mainline KLEE.

I've started trying upstreaming some of the work that came from adding
floating point support [1][2][3] but not the actual support it self
yet.
There's a bunch of stuff I want to get in mainline KLEE before I add
the floating point support.

At this point I'm impeded by KLEE's overly conservative review
process. Given that I have very little time is left to complete my PhD
there is a good chance that this work will never upstreamed (at least
by me anyway).

However the implementation (that is a fork of mainline KLEE) will
definitely be open sourced in the next few months and I would
certainly
like testers :)

[1] https://github.com/klee/klee/pull/657
[2] https://github.com/klee/klee/pull/658
[3] https://github.com/klee/klee/pull/629

Thanks,
Dan.