I am a PhD candidate in computer science at Cornell University, co-advised by David Bindel (Cornell) and Andrew Appel (Princeton). My current research primarily focuses on applying techniques from formal methods and programming languages to reason about the accuracy and correctness of numerical programs. As part of the VeriNum research group, I develop and maintain the VCFloat and LAProof libraries for the Coq Proof Assistant.

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

Affiliations

• PhD student, Department of Computer Science, Cornell University [Fall 2020 - current]. Advisor: David Bindel.
• Graduate student intern, Digital Foundations & Mathematics Department, Sandia National Laboratories [June 2021 - current]

Drafts

A Type System for Numerical Error Analysis. Ariel E. Kellison and Justin Hsu. Paper Draft.

Conference & Journal Papers

2024. VCFloat2: Floating-point Error Analysis in Coq. Andrew W. Appel and Ariel E. Kellison. To appear in the proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2024), January 2024.

2023. LAProof: A Library of Formal Proofs of Accuracy and Correctness for Linear Algebra Programs. Ariel E. Kellison, Andrew W. Appel, Mohit Tekriwal, and David Bindel. To appear in proceedings of the 30th IEEE International Symposium on Computer Arithmetic (ARITH), September 2023. [Paper]

2023. Verified Correctness, Accuracy, and Convergence of a Stationary Iterative Linear Solver: Jacobi Method. Mohit Tekriwal, Andrew W. Appel, Ariel E. Kellison, Jean-Baptiste Jeannin, and David Bindel. To appear in proceedings of the 16th Conference on Intelligent Computer Mathematics (CICM), September 2023. [Paper]

2022. Global Stochastic Optimization of Stellarator Coil Configurations. Silke Glas, Misha Padidar, Ariel E. Kellison, and David Bindel. Journal of Plasma Physics. [Paper]

2022. A Machine-Checked Direct Proof of the Steiner-Lehmus Theorem. Ariel E. Kellison. In Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2022).[Paper]

2019. Implementing Euclid’s Straightedge and Compass Constructions in Type Theory. Ariel E. Kellison, Mark Bickford, and Robert Constable. Annals of Mathematics and Artificial Intelligence. [Paper]

Workshop & Position Papers

2022. Towards Verified Rounding-Error Analysis for Stationary Iterative Methods. Ariel E. Kellison, Mohit Tekriwal, Jean-Baptiste Jeannin, and Geoffrey Hulette. Correctness 2022: Sixth International Workshop on Software Correctness for HPC Applications, November 2022. [Paper]

2022. Verified Numerical Methods for Ordinary Differential Equations. Ariel E. Kellison and Andrew W. Appel. NSV’22: 15th International Workshop on Numerical Software Verification, August 2022. [Paper]

2021. Real(istic) Specifications of Software. Samuel D. Pollard, Ariel Kellison, John Bender, and Geoffrey C. Hulette. ASCR Workshop on the Science of Scientific-Software Development and Use, U.S. Department of Energy, Office of Advanced Scientific Computing Research, December 2021.

2021. Formal Methods-Based Certification Frameworks for Scientific Computing Applications. Ariel Kellison, Geoff C. Hulette, John Bender, Samuel D. Pollard, and Heidi K. Thornquist. ASCR Workshop on Cybersecurity and Privacy for Scientific Computing Ecosystems, U.S. Department of Energy, Office of Advanced Scientific Computing Research, November 2021.

Fellowships

• Department of Energy Computational Science Graduate Fellowship [Fall 2020 - current]

Teaching Experience

• Summer Lecturer, Cornell CS 1110 - Introduction to Computing Using Python [Summer 2020]

Education

• BSc with honors in astrophysics from UC Santa Cruz.