I am a Ph.D. student in computer science at Cornell University, co-advised by David Bindel (Cornell) and Andrew Appel (Princeton). My current research primarily focuses on applying formal methods techniques to numerical software. More broadly, I’m interested in developing and using automated and interactive proof systems for program verification, and applying these systems to scientific computing software stacks.

Affiliations

• Ph.D. 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]

Bibliography

2022. VCFloat2: Floating-point Error Analysis in Coq. Andrew W. Appel and Ariel E. Kellison. In Submission. [Draft]

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]

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]

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.

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]

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

I hold a BS with honors in astrophysics from UC Santa Cruz.