Scientific computing is used in many safety-critical areas, from designing and controlling aircraft, to predicting the climate. As such it is important to provide formal guarantees to the numerical results provided by scientific computing, by ensuring that the numerical solutions of differential equations are correct. Our work has focused on providing formally verified numerical solutions for ordinary differential equations, using interactive theorem provers. The results are fully end-to-end, in the sense that they formally prove that the solution computed by the C program is quantifiably close to the real solution of the differential equation. To achieve this, we combine formalization of traditional results from numerical analysis (such as the Lax equivalence theorem), with bounds on iterative methods and floating-point arithmetic, as well as formal C semantics. One challenge of formal verification for scientific computing is to make the formalizations more automatic, and general enough to apply to reasonably realistic scenarios. Another challenge for formal verification is to be relevant to the traditional scientific computing community. Since worst-case bounds are often too conservative in practice, we will discuss ideas on alternate results to formalize.

This is joint work with Mohit Tekriwal and Karthik Duraisamy (Michigan), David Bindel and Ariel Kellison (Cornell), Andrew Appel (Princeton), and Geoffrey Hulette (Sandia).