Static Analysis of Finite Precision Computations

DOI10.1007/978-3-642-18275-4_17zbMath1317.68116OpenAlexW3138624857MaRDI QIDQ3075485

Sylvie Putot, Eric Goubault

Publication date: 15 February 2011

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

Full work available at URL: https://doi.org/10.1007/978-3-642-18275-4_17

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (18)

Practical policy iterations. A practical use of policy iterations for static analysis: the quadratic case ⋮ Bit-precise verification of discontinuity errors under fixed-point arithmetic ⋮ A generalization of \(p\)-boxes to affine arithmetic ⋮ Formally-verified round-off error analysis of Runge-Kutta methods ⋮ Stabilizing Floating-Point Programs Using Provenance Analysis ⋮ Acceleration of the abstract fixpoint computation in numerical program analysis ⋮ A two-phase approach for conditional floating-point verification ⋮ Deductive verification of floating-point Java programs in KeY ⋮ Runtime abstract interpretation for numerical accuracy and robustness ⋮ An Accurate Join for Zonotopes, Preserving Affine Input/Output Relations ⋮ Checking Compatibility of Bit Sizes in Floating Point Comparison Operations ⋮ Impact of Accuracy Optimization on the Convergence of Numerical Iterative Methods ⋮ A zonotopic framework for functional abstractions ⋮ Formally verified roundoff errors using SMT-based certificates and subdivisions ⋮ Analysis of software patches using numerical abstract interpretation ⋮ Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions ⋮ Transformation of a PID controller for numerical accuracy ⋮ A certifying square root and division elimination

Uses Software

• Unnamed Item

Cites Work

• Static Analysis of Numerical Algorithms
• Handbook of Floating-Point Arithmetic
• Numerical Software with Result Verification
• Programming Languages and Systems
• The Lanczos and Conjugate Gradient Algorithms
• Verification, Model Checking, and Abstract Interpretation
• A zonotopic framework for functional abstractions
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Static Analysis of Finite Precision Computations