Automating the verification of floating-point programs

DOI10.1007/978-3-319-72308-2_7MaRDI QIDQ1630033zbMATH OpenOpenAlexFDO

Authors Clément Fumex, Claude Marché, Yannick Moy

Publication date 7 December 2018

Full work available at URL https://hal.inria.fr/hal-01534533/file/article.pdf

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Multi-prover 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
• Combining Coq and Gappa for Certifying Floating-Point Programs
• Verified compilation of floating-point computations

Cited in

(10)

• Correct approximation of IEEE 754 floating-point arithmetic for program verification
• Deductive verification of floating-point Java programs in KeY
• Counterexample- and simulation-guided floating-point loop invariant synthesis
• Stabilizing Floating-Point Programs Using Provenance Analysis
• Polynomial function intervals for floating-point software verification
• Programming Languages and Systems
• Multi-prover verification of floating-point programs
• Automatic Generation of Guard-Stable Floating-Point Code
• Hammering Floating-Point Arithmetic
• Formally verified roundoff error bounds on LogSumExp-based computations

Describes a project that uses

Uses Software

• Why3

This page was built for publication: Automating the verification of floating-point programs

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