FMitF: Track 1: Foundational Approaches for End-to-end Formal Verification of Computational Physics

Regents Of The University Of Michigan - Ann Arbor, Ann Arbor MI

Investigators

Abstract

Numerical solutions of differential equations are widely used in analysis and design tasks in science and engineering. Examples include modeling climate change, discovering new materials, designing aircraft, and understanding the early universe. This simulation process, however, involves errors arising from a number of sources such as the finiteness of the numerical discretization, potential lack of convergence of algorithms, floating-point arithmetic, and sampling required to quantify uncertainties. The project's novelties are a new formalism to ensure a rigorous handle over errors and uncertainties in numerical methods, and computer-checked proofs of the formalization and applications. The project's impact is a better understanding and quantification of the errors involved in scientific computations, leading to a higher confidence in simulation-informed analysis and design of natural and engineered systems. The current state of the art in numerical analysis relies on paper proofs. In practical implementations, the impact of rounding error is seldom quantified, and even when quantified, not formalized. The interplay with the implementation (C code level and below) is also not clearly assessed. Practitioners use intuitive techniques such as convergence tests and the method of manufactured solutions to manually check the viability of a numerical algorithm. Since these techniques yield necessary yet not sufficient checks, scientists rely on their expertise to guide applications. This work offers the possibility of the user setting a tolerable error threshold, and being assured of achieving it via their implementation in several computational physics tasks. The idea of bounding errors asymptotically is uncommon in formal methods, and will inevitably lead to the development of tools and techniques to better handle asymptotic guarantees in interactive theorem proving. As a side effect, this will expand and consolidate formal-methods libraries handling real arithmetic and limits. This work is expected to be transformational for computational physics, and spur the development of a sub-field at the intersection of formal methods and computational science. The proofs are mechanically checked in an interactive theorem prover using a variety of mathematical results ranging from convergence of functions to floating-point arithmetic and C semantics, thereby using various theories in one proof of correctness. The project creates a new space of physical applications to formal methods researchers, and for computational physicists to derive value from formalizing their programs. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.