Sound compilation of reals

DOI10.1145/2535838.2535874MaRDI QIDQ5408419zbMATH OpenOpenAlexFDO

Authors Eva Darulova, Viktor Kuncak

Publication date 10 April 2014

Published in Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1309.2511

zbMATH Keywords

compilationembedded systemsfixed-point arithmeticfloating-point arithmeticnumerical approximationroundoff errorscientific computingsensitivity analysisverification

Mathematics Subject Classification ID

Roundoff error (65G50) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Abstract: Writing accurate numerical software is hard because of many sources of unavoidable uncertainties, including finite numerical precision of implementations. We present a programming model where the user writes a program in a real-valued implementation and specification language that explicitly includes different types of uncertainties. We then present a compilation algorithm that generates a conventional implementation that is guaranteed to meet the desired precision with respect to real numbers. Our verification step generates verification conditions that treat different uncertainties in a unified way and encode reasoning about floating-point roundoff errors into reasoning about real numbers. Such verification conditions can be used as a standardized format for verifying the precision and the correctness of numerical programs. Due to their often non-linear nature, precise reasoning about such verification conditions remains difficult. We show that current state-of-the art SMT solvers do not scale well to solving such verification conditions. We propose a new procedure that combines exact SMT solving over reals with approximate and sound affine and interval arithmetic. We show that this approach overcomes scalability limitations of SMT solvers while providing improved precision over affine and interval arithmetic. Using our initial implementation we show the usefullness and effectiveness of our approach on several examples, including those containing non-linear computation.

Recommendations

• Polynomial function intervals for floating-point software verification
• Numerical Software with Result Verification
• Sound Numerical Computations in Abstract Acceleration
• Verified compilation of floating-point computations
• Hardware-Dependent Proofs of Numerical Programs

Cited in

(9)

• Combining tools for optimization and analysis of floating-point computations
• 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
• Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions
• Bit-precise verification of discontinuity errors under fixed-point arithmetic
• Synthesis of Rigorous Floating-Point Predicates
• Algorithm 1029: encapsulated error, a direct approach to evaluate floating-point accuracy
• Rigorous roundoff error analysis of probabilistic floating-point computations

This page was built for publication: Sound compilation of reals

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