Ariel Eileen Kellison

Applied Scientist at Code Metal

I design foundational tools with rigorous guarantees that make it convenient for programmers to reason about numerical accuracy and correctness. My research focuses on ensuring the trustworthiness of computational models by improving reliability and robustness.

I completed my PhD in computer science at Cornell in December 2024, where I developed novel static analysis techniques to verify the correctness and accuracy of numerical software. I was co-advised by David Bindel (Cornell) and Andrew Appel (Princeton). I was supported by the Department of Energy Computational Science Graduate Fellowship.

As part of the VeriNum research group, I maintain the VCFloat and LAProof libraries for the Coq Proof Assistant.

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

Dissertation

• Ariel E. Kellison. Type-Based Approaches to Rounding Error Analysis. PhD Thesis, Cornell University, December 2024.

Selected Publications

1. Ariel E. Kellison, Laura Zielinski, David Bindel, and Justin Hsu. Bean: A Language for Backward Error Analysis. Conditionally Accepted to PLDI, 2025.
2. Ariel E. Kellison and Justin Hsu. Numerical Fuzz: A Type System for Rounding Error Analysis. PLDI, 2024.
3. Andrew W. Appel and Ariel E. Kellison. VCFloat2: Floating-point Error Analysis in Coq. CPP, 2024.
4. 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