Runtime abstract interpretation for numerical accuracy and robustness

DOI10.1007/978-3-030-67067-2_12MaRDI QIDQ2234076zbMATH OpenOpenAlexFDO

Authors Franck Védrine, Maxime Jacquemin, Nikolai Kosmatov, Julien Signoles

Publication date 18 October 2021

Full work available at URL https://doi.org/10.1007/978-3-030-67067-2_12

Mathematics Subject Classification ID

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

Recommendations

• Programming Languages and Systems
• Sound compilation of reals
• scientific article; zbMATH DE number 2087547
• Static Analysis of Numerical Algorithms
• Sound Numerical Computations in Abstract Acceleration

Cites work

• A survey of challenges for runtime verification from advanced application domains (beyond software)
• An abstract interpretation framework for the round-off error analysis of floating-point programs
• CADNA: a library for estimating round-off error propagation
• Certification of bounds on expressions involving rounded operators
• Certified roundoff error bounds using semidefinite programming
• Cut branches before looking for bugs: certifiably sound verification on relaxed slices
• Grammar Analysis and Parsing by Abstract Interpretation
• Handbook of Floating-Point Arithmetic
• Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions
• Sound compilation of reals
• Static analysis of finite precision computations

Cited in

(3)

• FLDBox
• Programming Languages and Systems
• Abstract Semantic Differencing for Numerical Programs

Describes a project that uses

Uses Software

• FLDCompiler

This page was built for publication: Runtime abstract interpretation for numerical accuracy and robustness

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