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
Josh Cohen, Princeton University, PhD Student
Yichen Tao, Sahil Bola, University of Michigan, PhD Students
Shengyi Wang, Princeton University, Research Scientist
Mohit Tekriwal, Lawrence Livermore Lab, Postdoc, External Collaborator
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
- Verified correctness, accuracy, and convergence of a stationary iterative linear solver: Jacobi method, by Mohit Tekriwal, Andrew W. Appel, Ariel E. Kellison, David Bindel, and Jean-Baptiste Jeannin. 16th Conference on Intelligent Computer Mathematics, September 2023.
- LAProof: a library of formal accuracy and correctness proofs for sparse linear algebra programs, by Ariel E. Kellison, Andrew W. Appel, Mohit Tekriwal, and David Bindel, 30th IEEE International Symposium on Computer Arithmetic, September 2023.
- 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.
- 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, in CPP 2024: Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 14–29, January 2024.
- 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.
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