On Sound Compilation of Reals
Eva Darulova, Viktor Kuncak

TL;DR
This paper introduces a compilation and verification framework for numerical software that guarantees precision and correctness by modeling uncertainties explicitly and combining exact SMT solving with approximate methods.
Contribution
It presents a novel compilation algorithm and verification approach that unify uncertainty reasoning and improve scalability for verifying numerical programs.
Findings
Verification conditions can be used to check precision and correctness.
The combined approach improves scalability over pure SMT solving.
Effective on non-linear numerical examples.
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsNumerical Methods and Algorithms · Parallel Computing and Optimization Techniques · Formal Methods in Verification
