VeriNum

VeriNum

Andrew W. Appel, Princeton University

David Bindel, Cornell University

Jean-Baptiste Jeannin, University of Michigan

Karthik Duraisamy, University of Michigan


Ariel Kellison, Consultant

Yichen Tao, Sahil Bola, University of Michigan, PhD Students

Dennis Corraliza, Cornell University, PhD Student

Philip Johnson-Freyd, Samuel Pollard, Heidi Thornquist, Sandia National Labs, External Collaborators

Alumni: Mohit Tekriwal, Michigan, PhD Student; Josh Cohen, PhD Student


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