A Mechanized Error Analysis Framework for End-to-End Verification of Numerical Programs

Abstract

The behavior of physical systems is usually modeled by differential equations. For instance, the aerodynamics of airplanes is modeled by the Navier-Stokes equation; problems of optimal control are modeled by the Ricatti differential equation; and the valuation of stock options is modeled by the Black-Scholes equation. Thus, differential equations are pervasive in almost every aspect of science and engineering, and being able to solve them precisely and accurately, but also while trusting that the solutions are accurate, is of utmost importance. Since many of these differential equations are mostly difficult or intractable to solve analytically, they are typically solved numerically. This leads to an accumulation of errors at each approximation step. In the past, this accumulation of errors has led to catastrophic consequences like the failure of the Patriot missile system due to floating-point errors; and the infamous multi-million dollar loss in the Vancouver stock exchange due to accumulation of floating-point errors. It is thus important that we analyze each approximation error rigorously and formalize conditions which could lead to unexpected divergent behaviors of numerical solvers.

In my thesis, I propose a mechanized error analysis framework, which treats errors from each approximation step modularly, in a formal setting like the Coq theorem prover. This framework connects a differential equation to the actual implementation of a linear solver for computing solutions to a differential equation. We show convergence of a finite-difference method, which is used to discretize the differential equation; compute an approximated solution to the discretized set of equations using stationary iterative methods, and prove its convergence formally in the field of reals. We then extend this analysis to a concrete implementation of a stationary iterative algorithm: Jacobi iteration, and prove correctness, accuracy and convergence of the implementation in the presence of floating-point errors. Our floating-point error analysis takes into account exceptional floating-point behaviors including overflow and underflow, and we prove the absence of overflow at each iteration by deriving concrete bounds on the input variables to the algorithm.

Some of the important contributions of this thesis include: the formalization of a generic statement about convergence for finite-difference methods -- the Lax-equivalence theorem; the formalization of a generic statement about iterative convergence in the field of reals; the formalization of properties of the $l^2$ and $l^infty$ matrix and vector norms; norm-wise forward error bounds for matrix-vector operations in floating-point arithmetic; and the demonstration of a modular approach to achieve program verification on the Jacobi iteration method. This thesis further proposes ways to extend our end-to-end verification framework beyond Jacobi iteration to any stationary iterative method, and proposes ways in which automation could be achieved, as future extensions of this work.