A two-phase approach for conditional floating-point verification

DOI10.1007/978-3-030-72013-1_3MaRDI QIDQ2233493zbMATH OpenOpenAlexFDO

Authors Debasmita Lohar, Clothilde Jeangoudoux, Joshua Sobel, Eva Darulova, Maria Christakis

Publication date 18 October 2021

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-72013-1_3

Mathematics Subject Classification ID

Roundoff error (65G50) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Multi-prover verification of floating-point programs
• Numerical Software with Result Verification
• Correct approximation of IEEE 754 floating-point arithmetic for program verification
• scientific article; zbMATH DE number 2087547
• Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions

Cites work

• scientific article; zbMATH DE number 1953274 (Why is no real title available?)
• A formal analysis of the compact position reporting algorithm
• A parameterized floating-point formalizaton in HOL Light
• Automatic detection of floating-point exceptions
• Certified roundoff error bounds using semidefinite programming
• Certifying the Floating-Point Implementation of an Elementary Function Using Gappa
• Combining Coq and Gappa for Certifying Floating-Point Programs
• Compositional may-must program analysis: unleashing the power of alternation
• Containment control of a class of heterogeneous nonlinear multi-agent systems
• Deciding floating-point logic with abstract conflict driven clause learning
• Fast polyhedra abstract domain
• Grammar Analysis and Parsing by Abstract Interpretation
• Introduction to Interval Analysis
• Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions
• Rigorous floating-point mixed-precision tuning
• Sound compilation of reals
• Static analysis of finite precision computations
• Wave equation numerical resolution: a comprehensive mechanized proof of a C program

Cited in

(8)

• Eliminating unstable tests in floating-point programs
• Automatic detection of floating-point exceptions
• Deductive verification of floating-point Java programs in KeY
• Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions
• Counterexample- and simulation-guided floating-point loop invariant synthesis
• Combining tools for optimization and analysis of floating-point computations
• Programming Languages and Systems
• Model checking linear dynamical systems under floating-point rounding

This page was built for publication: A two-phase approach for conditional floating-point verification

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