Multi-prover verification of floating-point programs

DOI10.1007/978-3-642-14203-1_11MaRDI QIDQ5747756zbMATH OpenOpenAlexFDO

Authors Ali Ayad, Claude Marché

Publication date 14 September 2010

Published in Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-14203-1_11

Mathematics Subject Classification ID

Recommendations

• Automating the verification of floating-point programs
• Deductive verification of floating-point Java programs in KeY
• Correct approximation of IEEE 754 floating-point arithmetic for program verification
• Verified compilation of floating-point computations
• Combining Coq and Gappa for Certifying Floating-Point Programs

Cites work

• \textsf{CC(X)}: semantic combination of congruence closure with solvable theories
• A mechanically checked proof of the AMD5/sub K/86/sup TM/ floating-point division program
• Automatic modular abstractions for linear constraints
• Efficient E-Matching for SMT Solvers
• scientific article; zbMATH DE number 1863384 (Why is no real title available?)
• Multi-prover verification of floating-point programs
• Proving Bounds on Real-Valued Functions with Computations

Cited in

(19)

• Automating the verification of floating-point programs
• Formal verification of numerical programs: from C annotated programs to mechanical proofs
• TASS: the toolkit for accurate scientific software
• Computer-assisted verification of four interval arithmetic operators
• A two-phase approach for conditional floating-point verification
• Deductive verification of floating-point Java programs in KeY
• Verified compilation of floating-point computations
• Stabilizing Floating-Point Programs Using Provenance Analysis
• Hardware-Dependent Proofs of Numerical Programs
• Combining Coq and Gappa for Certifying Floating-Point Programs
• Floats and Ropes: A Case Study for Formal Numerical Program Verification
• scientific article; zbMATH DE number 67109 (Why is no real title available?)
• A mechanically checked proof of the AMD5/sub K/86/sup TM/ floating-point division program
• Polynomial function intervals for floating-point software verification
• Deciding floating-point logic with abstract conflict driven clause learning
• C-language floating-point proofs layered with VST and Flocq
• Multi-prover verification of floating-point programs
• Synthesis of Rigorous Floating-Point Predicates
• Formally verified roundoff error bounds on LogSumExp-based computations

Describes a project that uses

Uses Software

• ACL2
• Coq
• KRAKATOA
• Yices
• Why3
• Spec#
• Caduceus
• Frama-C
• cvc3
• z3
• HOL Light

This page was built for publication: Multi-prover verification of floating-point programs

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