[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

From: Tim Daly
Subject: [Axiom-developer] Proving Axiom Sane [PAS]: Bagn19 paper
Date: Mon, 25 Mar 2019 00:26:39 -0400

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.


reply via email to

[Prev in Thread] Current Thread [Next in Thread]