[klee-dev] Will KLEE Be Able to Do Floating-Point Error Reasoning?

[Andrew Santosa]

Many thanks to Cristian for his reply to my previous question in this thread:
Re: [klee-dev] Floating-Point Symbolic Execution


|   |
|   |  |   |   |   |   |   |
| Re: [klee-dev] Floating-Point Symbolic ExecutionHi 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... |
|  |
| View on www.mail-archive.com | Preview by Yahoo |
|  |
|   |


Today I have just  read a paper from 2008 on FPInsthttp://www.freearrow.com/downloads/files/fpinst.pdf
On Page 9, the authors seem to argue against the use of LLVM IR for floating-point error reasoning due to imprecision issues.I am wondering if floating point error analysis is an application area that is being considered in the KLEE floating-point supportcurrently being worked on?
Thank you in advance.

Best,Andrew
-------------- next part --------------
HTML attachment scrubbed and removed