An abstract interpretation framework for the round-off error analysis of floating-point programs

DOI10.1007/978-3-319-73721-8_24MaRDI QIDQ3296349zbMATH OpenOpenAlexFDO

Authors Laura Titolo, Marco A. Feliú, Mariano M. Moscato, César Muñoz

Publication date 7 July 2020

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://hdl.handle.net/2060/20180006290

Mathematics Subject Classification ID

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

Recommendations

• Certified roundoff error bounds using semidefinite programming
• scientific article; zbMATH DE number 2087547
• scientific article; zbMATH DE number 2087546
• Semantics of roundoff error propagation in finite precision calculations
• Numerical Software with Result Verification

Cited in

(17)

• Formal analysis of the compact position reporting algorithm
• Exploiting verified neural networks via floating point numerical error
• Formal analysis of the application programming interface of the PVS verification system
• Runtime abstract interpretation for numerical accuracy and robustness
• Certified roundoff error bounds using semidefinite programming
• scientific article; zbMATH DE number 2087546 (Why is no real title available?)
• scientific article; zbMATH DE number 2087547 (Why is no real title available?)
• Programming Languages and Systems
• PRECiSA
• Bit-precise verification of discontinuity errors under fixed-point arithmetic
• Synthesis of Rigorous Floating-Point Predicates
• Provably correct floating-point implementation of a point-in-polygon algorithm
• Formally verified roundoff errors using SMT-based certificates and subdivisions
• Algorithm 1029: encapsulated error, a direct approach to evaluate floating-point accuracy
• Embedding differential dynamic logic in PVS
• Taming floating-point rounding errors with proofs (invited talk)
• Rigorous roundoff error analysis of probabilistic floating-point computations

Describes a project that uses

Uses Software

• ASTREE
• RangeLab
• PVS
• HOL Light
• Frama-C

This page was built for publication: An abstract interpretation framework for the round-off error analysis of floating-point programs

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