scientific article; zbMATH DE number 1979556

MaRDI QIDQ4427909zbMATH OpenFDO

Authors Jun Sawada, Ruben A. Gamboa

Publication date 14 September 2003

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2517/25170274.htm

Mathematics Subject Classification ID

Recommendations

• Formal verification of square root algorithms
• Formal Verification of Transcendental Fixed- and Floating-point Algorithms using an Automatic Theorem Prover
• A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7^™ Processor
• A proof of GMP square root
• scientific article; zbMATH DE number 1670746

Cited in

(4)

• Theory extension in ACL2(r)
• Formal Verification of Exact Computations Using Newton’s Method
• Formal verification of Medina's sequence of polynomials for approximating arctangent
• Formalization of fixed-point arithmetic in HOL

Describes a project that uses

Uses Software

• ACL2

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4427909)