Asserting the precision of floating-point computations: A simple abstract interpreter

DOI10.1007/3-540-45927-8_15MaRDI QIDQ4738356zbMATH OpenFDO

Authors Éric Goubault, Matthieu Martel, Sylvie Putot

Publication date 11 August 2004

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

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2305/23050209.htm

Mathematics Subject Classification ID

Roundoff error (65G50) Theory of software (68N99)

Recommendations

• Numerical Software with Result Verification
• Static analyses of the precision of floating-point operations
• Static analysis of finite precision computations
• An abstract interpretation framework for the round-off error analysis of floating-point programs
• Floating-point numbers with error estimates

Cited in

(27)

• FEVS: a functional equivalence verification suite for high-performance scientific computing
• Combining tools for optimization and analysis of floating-point computations
• Correct approximation of IEEE 754 floating-point arithmetic for program verification
• A two-phase approach for conditional floating-point verification
• Runtime abstract interpretation for numerical accuracy and robustness
• Abstract fixpoint computations with numerical acceleration methods
• Automatic detection of floating-point exceptions
• Static analysis of finite precision computations
• An abstract interpretation framework for the round-off error analysis of floating-point programs
• Acceleration of the abstract fixpoint computation in numerical program analysis
• Propagation of roundoff errors in finite precision computations: A semantics approach
• Static analyses of the precision of floating-point operations
• Deciding floating-point logic with abstract conflict driven clause learning
• Checking compatibility of bit sizes in floating point comparison operations
• Inferring effective types for static analysis of C programs
• Numerical Software with Result Verification
• Programming Languages and Systems
• Abstract Interpretation of the Physical Inputs of Embedded Programs
• A Hybrid Denotational Semantics for Hybrid Systems
• Eliminating unstable tests in floating-point programs
• Synthesis of Rigorous Floating-Point Predicates
• Relative precision in the inductive assertion method
• Floating-point numbers with error estimates
• Enhancing the implementation of mathematical formulas for fixed-point and floating-point arithmetics
• Why does Astrée scale up?
• Termination of floating-point computations
• Semantics of roundoff error propagation in finite precision calculations

This page was built for publication: Asserting the precision of floating-point computations: A simple abstract interpreter

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