VeriNum
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
Bibliography
- 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.
Funding
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