Andrew W. Appel, Princeton University
David Bindel, Cornell University
Geoff Hulette, Sandia National Labs
Ariel Kellison, Cornell University
Josh Cohen, Princeton University
Tim Carstens, RISC Zero
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
Our initial research projects (and results) are,
- 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, to appear 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.
- A Unified Coq Framework for Verifying C Programs with Floating-Point Computations, by Tahina Ramananandro, Paul Mountcastle, Benoit Meister, and Richard Lethin, CPP’16: 5th ACM SIGPLAN Conference on Certified Programs and Proofs, pages 15-26, 2016.
VeriNum’s various projects are supported in part by
- The National Science Foundation for the grant “Collaborative Research: FMitF: Track I: Formally Verified Numerical Methods”, to Princeton University (Appel, Principal Investigator) and Cornell University (Bindel)
- Sandia National Laboratories, funding the collaboration of Dr. Geoffrey Hulette with these projects
- U.S. Department of Energy Computational Science Graduate Fellowship (Ariel Kellison)