Formal Verification of Transcendental Fixed- and Floating-point Algorithms using an Automatic Theorem Prover

DOI10.1145/3543670zbMATH Open1522.68306OpenAlexW4282832561WikidataQ113769892 ScholiaQ113769892MaRDI QIDQ6136749FDOQ6136749

Theo A. Drane, Lawrence C. Paulson, Author name not available (Why is that?), Author name not available (Why is that?)

Publication date: 31 August 2023

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/3543670

Recommendations

• scientific article; zbMATH DE number 1670746
• Formal verification of the VAMP floating point unit
• Computer arithmetic and formal proofs. Verifying floating-point algorithms with the Coq system
• scientific article; zbMATH DE number 1614683
• Formal Methods in Computer-Aided Design

zbMATH Keywords

theorem provertranscendental functionsfloating-point algorithms

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cited In (7)

• Formal Methods in Computer-Aided Design
• Title not available (Why is that?)
• Title not available (Why is that?)
• Formal Verification of Exact Computations Using Newton’s Method
• Formal analysis of the Schulz matrix inversion algorithm: a paradigm towards computer aided verification of general matrix flow solvers
• Title not available (Why is that?)
• Title not available (Why is that?)

This page was built for publication: Formal Verification of Transcendental Fixed- and Floating-point Algorithms using an Automatic Theorem Prover

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