Sat 17 Jun 2023 11:20 - 12:00 at Magnolia 1-3 - CSC: Open Session 2

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

Sat 17 Jun

Displayed time zone: Eastern Time (US & Canada) change

11:20 - 12:30
Formal Verification in Scientific ComputingInvited Talk
Jean-Baptiste Jeannin University of Michigan at Ann Arbor
Lightning Talks
Laura Titolo NIA/NASA LaRC, Aditya V. Thakur University of California at Davis