Mechanical verification of a square root algorithm using Taylor's theorem

DOI10.1007/3-540-36126-X_17MaRDI QIDQ4427909zbMATH OpenFDO

Authors Jun Sawada, Ruben A. Gamboa

Publication date 14 September 2003

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

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
• Formal verification of IA-64 division algorithms

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: Mechanical verification of a square root algorithm using Taylor's theorem

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