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

(15)

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

Describes a project that uses

Uses Software

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

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)