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 _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer
