Proving Axiom Sane [PAS]: Bagn19 paper

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
1 message Options
Reply | Threaded
Open this post in threaded view
|

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

_______________________________________________
Axiom-developer mailing list
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer