Synthesis of Rigorous Floating-Point Predicates

DOI10.1007/978-3-031-15077-7_3zbMATH Open1514.6804MaRDI QIDQ6487299FDOQ6487299

Authors: Thanh-Son Nguyen, Ben Jones 

Publication date: 7 December 2022

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

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (4)

• Deciding floating-point logic with abstract conflict driven clause learning
• Formally certified floating-point filters for homogeneous geometric predicates
• Counterexample- and simulation-guided floating-point loop invariant synthesis
• Title not available (Why is that?)

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)