[klee-dev] Floating-Point Symbolic Execution

[Cristian Cadar]

Hi Andrew,

KLEE-FP/KLEE-CL (https://srg.doc.ic.ac.uk/projects/klee-cl/) is targeted 
primarily toward cross-checking of (purportedly) equivalent FP code, 
although it has some basic integration with a FP solver from CBMC.

Dan Liew, Alastair Donaldson and I are working on full FP support for 
KLEE on top of Z3, but this is still work in progress.  I don't 
anticipate having anything ready until the end of the year.

Best,
Cristian

On 27/05/16 14:42, Andrew Santosa wrote:
> Dear All,
>
> In KLEE, it seems symbolic floating point variables are simply converted
> to int and grounded to 0. I am wondering
> what is the current state of floating point symbolic execution support
> in KLEE? I know there has been some work
> on KLEE-FP in the past, but does it actually check path feasibility via
> path condition satisfiability in QF_FPA?
> Now that KLEE supports Z3 as backend solver, perhaps such feasibility
> checking is not too difficult to implement?
>
> Best,
> Andrew
>
>
>
>
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>