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,



VeriNum’s various projects are supported in part by