Formal verification of square root algorithms

DOI10.1023/A:1022973506233MaRDI QIDQ1870226zbMATH OpenOpenAlexFDO

Authors Yanyan Li

Publication date 11 May 2003

Published in Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1023/a:1022973506233

zbMATH Keywords

automated theorem provingformal verificationfloating-point arithmetic

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65)

Recommendations

• A proof of GMP square root
• scientific article; zbMATH DE number 1670746
• scientific article; zbMATH DE number 1614683
• Verification: industrial applications
• A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7^™ Processor

Cited in

(11)

• A Formal Proof of Square Root and Division Elimination in Embedded Programs
• Deciding floating-point logic with abstract conflict driven clause learning
• Computation and Formal Verification of SRT Quotient and Square Root Digit Selection Tables
• scientific article; zbMATH DE number 1614683 (Why is no real title available?)
• Formal specification of MPI 2.0: case study in specifying a practical concurrent programming API
• scientific article; zbMATH DE number 1670746 (Why is no real title available?)
• A Why3 proof of GMP algorithms
• Verification: industrial applications
• Formal Verification of Exact Computations Using Newton’s Method
• Mutation-Based Test Case Generation for Simulink Models
• scientific article; zbMATH DE number 1979556 (Why is no real title available?)

Describes a project that uses

Uses Software

• HOL Light

This page was built for publication: Formal verification of square root algorithms

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