Proving Axiom Sane [PAS]: Bagn19 paper

Tim Daly <[email protected]> Mon, 25 Mar 2019 00:26:39 -0400

Newsgroups	gmane.comp.mathematics.axiom.devel
Message-ID	<CAJn5L=LqW+UTr_+jmLUOUErkW46v+pwy=op36d6VEtiArcj_9A@mail.gmail.com>

Roberto Bagnara, Abramo Bagnara, Fabio Biselli, Michele Chiari, and Roberta Gori
"Correct Approximation of IEEE 754 Floating-Point Arithmetic for
Program Verification"

an interesting read as well as a good example of using TAC (three-address code)
and SSA (static single assignment) in proofs. This allows constraint propagation
and constrained solutoins.

Well worth the read.

Tim