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.


Axiom-developer mailing list
[hidden email]