Andrew W. Appel, Princeton University

David Bindel, Cornell University

Jean-Baptiste Jeannin, University of Michigan

Karthik Duraisamy, University of Michigan

Ariel Kellison, Cornell University, *PhD Student*

Mohit Tekriwal, University of Michigan, *PhD Student*

Josh Cohen, Princeton University, *PhD Student*

Shengyi Wang, Princeton University, *Postdoc*

Philip Johnson-Freyd, Samuel Pollard, Heidi Thornquist, Sandia National Labs, *External Collaborators*

In this collection of research projects, we take a layered approach to foundational verification of correctness and accuracy of numerical software–that is, formal machine-checked proofs about programs (not just algorithms), with no assumptions except specifications of instruction-set architectures. We build, improve, and use appropriate tools at each layer: proving in the real numbers about discrete algorithms; proving how floating-point algorithms approximate real-number algorithms; reasoning about C program implementation of floating-point algorithms; and connecting all proofs end-to-end in Coq.

Our initial research projects (and results) are,

- cbench_vst/sqrt: Square root by Newton’s Method, by Appel and Bertot.
- VerifiedLeapfrog: A verified numerical method for an Ordinary Differential Equation, by Kellison and Appel.
- VCFloat2: Floating-point error analysis in Coq, by Appel & Kellison, improvements on an earlier open-source project by Ramananandro et al.
- Parallel Dot Product, demonstrating how to use VST to verify correctness of simple shared-memory task parallelism
- Stationary Iterative Methods with formally verified error bounds

- C-language floating-point proofs layered with VST and Flocq, by Andrew W. Appel and Yves Bertot,
*Journal of Formalized Reasoning*volume 13, number 1, pages 1-16. - Verified Numerical Methods for Ordinary Differential Equations, by Ariel E. Kellison and Andrew W. Appel, in
*NSV’22: 15th International Workshop on Numerical Software Verification*, August 2022. - VCFloat2: Floating-point Error Analysis in Coq, by Andrew W. Appel and Ariel E. Kellison, draft, April 2022.
- Towards verified rounding error analysis for stationary iterative methods, by Ariel Kellison, Mohit Tekriwal, Jean-Baptiste Jeannin, and Geoffrey Hulette, in
*Correctness 2022: Sixth International Workshop on Software Correctness for HPC Applications*, November 2022.

VeriNum’s various projects are supported in part by

- National Science Foundation grant 2219757 “Formally Verified Numerical Methods”, to Princeton University (Appel, Principal Investigator) and grant 2219758 to Cornell University (Bindel)
- National Science Foundation grant 2219997 “Foundational Approaches for End-to-end Formal Verification of Computational Physics” to the University of Michigan (Jeannin and Duraisamy)
- U.S. Department of Energy Computational Science Graduate Fellowship (Ariel Kellison)
- Sandia National Laboratories, funding the collaboration of Sandia participants with these projects