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.)
-
From 2016. http://www.kroening.com/papers/fm2016-float.pdf … And it mentions some other work on page 1 and other cites.
Wow. This looks amazing! Thanks! I think I need to download VerifOx and try to reproduce their result. (Last time I tried v2c it just crashed on me on all non-trivial inputs. But luckily I can also do the Verilog -> C transformation with Yosys.)