https://www.cambridge.org/core/journals/lms-journal-of-computation-and-mathematics/article/div-classtitlea-mechanically-checked-proof-of-ieee-compliance-of-the-floating-point-multiplication-division-and-square-root-algorithms-of-the-amd-k7span-classsupspan-processordiv/5C4FBB3FE20712D8FD5070AFEC096ED9 … This might be transferable to SMT?
Does anyone have good references for state of the art for *automated* correctness proofs for FPUs? (By that I mean stuff like transferable black-box proofs using SMT solvers, not white-box proofs utilizing Coq and 1-3 person-year cheap labor from someone who wants to get a PhD.)
-
-
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
From 2016. http://www.kroening.com/papers/fm2016-float.pdf … And it mentions some other work on page 1 and other cites.
-
Hello :o!! This looks awesome!
End of conversation
New conversation -
-
-
Perhaps the following works (or citations therein) can be of use: http://www.cs.ox.ac.uk/tom.melham/pub/Seger-2005-IEE.pdf …, https://is.muni.cz/el/1433/jaro2010/IA159/um/intel.pdf …, https://s3.amazonaws.com/verificationacademy-news/DVCon2017/Papers/dvcon-2017_efficient-and-exhaustive-floating-point-verification-using-sequential-equivalence-checking_paper.pdf ….
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
We provide C-RTL bug hunting and proving, free for open source FPU. https://github.com/exa-mining/oss-c-rtl …
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.