Synthesis of Rigorous Floating-Point Predicates

DOI10.1007/978-3-031-15077-7_3MaRDI QIDQ6487299zbMATH OpenFDO

Authors Thanh-Son Nguyen, Ben Jones

Publication date 7 December 2022

Mathematics Subject Classification ID

Roundoff error (65G50) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Formal Methods for Hardware Verification
• scientific article; zbMATH DE number 67109
• Multi-prover verification of floating-point programs
• Computer arithmetic and formal proofs. Verifying floating-point algorithms with the Coq system
• Verified compilation of floating-point computations
• scientific article; zbMATH DE number 2087547
• Verification methods: rigorous results using floating-point arithmetic
• A three-tier strategy for reasoning about floating-point numbers in SMT

Cites work

• scientific article; zbMATH DE number 3281219 (Why is no real title available?)
• A floating-point technique for extending the available precision
• Adaptive precision floating-point arithmetic and fast robust geometric predicates
• An abstract interpretation framework for the round-off error analysis of floating-point programs
• Automatic generation of staged geometric predicates
• Future paths for integer programming and links to artificial intelligence
• Interval arithmetic yields efficient dynamic filters for computational geometry
• Sound compilation of reals

Cited in

(4)

• Counterexample- and simulation-guided floating-point loop invariant synthesis
• Formally certified floating-point filters for homogeneous geometric predicates
• Deciding floating-point logic with abstract conflict driven clause learning
• scientific article; zbMATH DE number 67109 (Why is no real title available?)

This page was built for publication: Synthesis of Rigorous Floating-Point Predicates

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