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

[Dan Liew]

Hi,

On 12 June 2017 at 13:12, Henrik Tjäder  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.

Just to note my fork of KLEE that supports floating point arithmetic
is now open source [1].
You can build it is as normal but you

* Have to build using CMake
* You have to build with Z3 support and use that as the constraint solver.

The intention is to eventually upstream this implementation along with
the implementation
of one of my collaborators [2]. It will be several months before this
happens though.

Have fun,
Dan

[1] https://github.com/srg-imperial/klee-float
[2] https://github.com/danielschemmel/klee-z3float-aachen

___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

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

[Dan Liew]

Hi,

On 12 June 2017 at 13:12, Henrik Tjäder  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.

___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

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

[Henrik Tjäder]

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.

Best regards,
Henrik Tjäder

(1) - http://www.mail-archive.com/klee-dev@imperial.ac.uk/msg02517.html


___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev