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 Approach

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.

Key Features of the Verification Approach

1. Modular: The verification approach will be modular.
2. Automated: It will integrate with verification of non-accuracy properties.
3. Safe Optimizations: It will allow safe program optimizations for real-world programs.

Debugging Techniques

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

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