Formal verification of IA-64 division algorithms

DOI10.1007/3-540-44659-1_15MaRDI QIDQ2754046zbMATH OpenFDO

Authors John R. Harrison

Publication date 18 December 2001

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

Full work available at URL https://doi.org/10.1007/3-540-44659-1_15

Mathematics Subject Classification ID

Roundoff error (65G50) Numerical algorithms for specific classes of architectures (65Y10)

Recommendations

• Formal verification of square root algorithms
• scientific article; zbMATH DE number 139976
• Formal verification of the VAMP floating point unit
• Formal Verification of Transcendental Fixed- and Floating-point Algorithms using an Automatic Theorem Prover

Cited in

(24)

• Proof assistants: history, ideas and future
• A proof of the nonrestoring division algorithm and its implementation on an ALU
• How to get an efficient yet verified arbitrary-precision integer library
• Formal verification of square root algorithms
• Embedded software verification using symbolic execution and uninterpreted functions
• WhyMP, a formally verified arbitrary-precision integer library
• Verified optimization for the Intel IA-64 architecture
• Formal proof of integer adders using all-prefix-sums operation
• scientific article; zbMATH DE number 139976 (Why is no real title available?)
• Mechanical verification of a square root algorithm using Taylor's theorem
• A mechanically checked proof of the AMD5/sub K/86/sup TM/ floating-point division program
• The formal derivation of algorithm and automatic verification based on Isabelle
• Applications of real number theorem proving in PVS
• Proof engineering in the large: Formal verification of Pentium^ 4 floating-point divider
• A formal proof of square root and division elimination in embedded programs
• Formalizing SPARCv8 instruction set architecture in Coq
• Computer Aided Verification
• A trustworthy monadic formalization of the ARMv7 instruction set architecture
• Formal proof of prefix adders
• Formal Verification of Transcendental Fixed- and Floating-point Algorithms using an Automatic Theorem Prover
• Formal verification of n-bit ALU using theorem proving
• Graph sequence learning for premise selection
• Verified implementation of an efficient term-rewriting algorithm for multiplier verification on ACL2
• Formalization of fixed-point arithmetic in HOL

Describes a project that uses

Uses Software

• HOL Light

This page was built for publication: Formal verification of IA-64 division algorithms

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