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

[Andrew Santosa]

Sorry, following is the correct link to the previous email thread that I mentioned
(which may have disappeared from my email).

http://www.mail-archive.com/klee-dev@imperial.ac.uk/msg02334.html

Best,
Andrew

On Friday, 17 June 2016, 11:50, Andrew Santosa <santosa_1999 at yahoo.com> wrote:

Many thanks to Cristian for his reply to my previous question in this thread:

Re: [klee-dev] Floating-Point Symbolic Execution  

Today I have just  read a paper from 2008 on FPInst
http://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 support
currently being worked on?

Thank you in advance.


Best,
Andrew