Multi-Prover Verification of Floating-Point Programs

DOI10.1007/978-3-642-14203-1_11zbMath1291.68321OpenAlexW1824011918MaRDI QIDQ5747756

Claude Marché, Ali Ayad

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

Related Items (7)

Computer-assisted verification of four interval arithmetic operators ⋮ Formal verification of numerical programs: from C annotated programs to mechanical proofs ⋮ TASS: the toolkit for accurate scientific software ⋮ Deciding floating-point logic with abstract conflict driven clause learning ⋮ Multi-Prover Verification of Floating-Point Programs ⋮ Hardware-Dependent Proofs of Numerical Programs ⋮ Verified compilation of floating-point computations

Uses Software

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

Cites Work

• Unnamed Item
• CC(X): Semantic Combination of Congruence Closure with Solvable Theories
• Proving Bounds on Real-Valued Functions with Computations
• Efficient E-Matching for SMT Solvers
• A mechanically checked proof of the AMD5/sub K/86/sup TM/ floating-point division program
• Automatic modular abstractions for linear constraints
• Multi-Prover Verification of Floating-Point Programs

This page was built for publication: Multi-Prover Verification of Floating-Point Programs