Ariel Eileen Kellison

Postdoctoral Researcher at Sandia National Labs

My goal is to help people build reliable numerical software. I design foundational tools with rigorous guarantees that make it convenient for programmers to reason about numerical accuracy and correctness. As part of the VeriNum research group, I maintain the VCFloat and LAProof libraries for the Coq Proof Assistant.

I completed my PhD in computer science at Cornell in December 2024. During my PhD, I was co-advised by David Bindel (Cornell) and Andrew Appel (Princeton). I was supported by the Department of Energy Computational Science Graduate Fellowship.

I can be reached by email at ak2485@cornell.edu.

Selected Publications

1. Ariel E. Kellison and Justin Hsu. Numerical Fuzz: A Type System for Rounding Error Analysis. PLDI, 2024.
2. Andrew W. Appel and Ariel E. Kellison. VCFloat2: Floating-point Error Analysis in Coq. CPP, 2024.
3. Ariel E. Kellison, Andrew W. Appel, Mohit Tekriwal, and David Bindel. LAProof: A Library of Formal Proofs of Accuracy and Correctness for Linear Algebra Programs. ARITH, 2023.

Selected Reports

1. S. D. Pollard, J. M. Aytac, A. Kellison, I. Laguna, S. Nedunuri, S. Reis, M. J. Sottile, and H. K. Thornquist. The first tri-lab workshop on formal verification: Capabilities, challenges, research opportunities, and exemplars. Technical report, Sandia National Laboratories, 2024.

Service

Education