[Axiom-developer] Proving Axiom Sane [PAS]: Bagn19 paper

[Tim Daly]

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