On Sound Compilation of Reals

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 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.