Skip to content

Latest commit

 

History

History
60 lines (42 loc) · 4.96 KB

README.md

File metadata and controls

60 lines (42 loc) · 4.96 KB

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,

Bibliography

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