Holistic Rigorous Numerical Verification

Introduction

My goal is to make rigorous numerical verification widely applicable and practically usable. Rigorous verification proves at compile-time that a program computes for all valid inputs what it is expected to. It is especially important for numerical programs, which are widely used across application domains and are often safety-critical.

Challenges in Numerical Verification

However, automated verification of numerical programs over finite-precision (e.g. floating-point) numbers is currently limited. Finite precision introduces rounding errors with respect to an ideal, real-valued specification and poses unique challenges for verification of program accuracy and other kinds of desirable properties.

As a result, verification of non-trivial numerical programs today requires extensive expert knowledge and mostly manual proofs. Additionally, when verification fails, e.g. because a program is buggy, developers have little debugging help available.

Proposed Solutions

I will rethink automated verification and debugging techniques for numerical programs from the ground up with accuracy as a core property. I propose a novel approach for accuracy verification based on deductive relational reasoning that will be able to effectively bound the difference between the specified (real-valued) and actually computed (finite-precision) program results.

Features of the Verification Approach

My verification approach will be:

1. Modular
2. Automated
3. Integrated with verification of non-accuracy properties
4. Allowing safe program optimizations for real-world programs

To further ensure the practical usability of the verifier, I will develop complementary techniques that will help developers to debug unsuccessful verification attempts by:

• Helping to fix specifications
• Localizing faults in the program
• Communicating effectively with the verifier

Expertise and Background

I will build on my comprehensive expertise with automated rigorous accuracy analysis and optimization of finite-precision arithmetic, and my recent efforts in deductive verification of floating-point runtime errors and numerical specification inference.