Broadly speaking, I am interested in the intersection of mathematics and computer science. More specifically, I am interested in formally verifying mathematical results and algorithms that have safety-critical applications. I typically work in the theorem prover Isabelle/HOL; you can find my AFP entries here.
In graduate school, I focused on formalizing algorithms for real quantifier elimination in Isabelle/HOL (my thesis topic). I also considered other topics that are relevant to the formal verification of cyber-physical systems (CPS): namely, efficient invariant generation and modeling (specifically, how to write models of CPS that build an awareness of physics into logic). My graduate school work was generously supported by an NSF Graduate Research Fellowship.
Prior to graduate school, I did research in various areas of mathematics. My Erdős number is 3.
Publications
My maiden name was Cordwell, and so my publications before 2022 appear under K. Cordwell.
Conference Papers
K. Kosaian, Y. K. Tan, and A. Platzer. A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL. Certified Programs and Proofs (CPP) 2023. (doi | arXiv | AFP | talk)
M. Scharager, K. Cordwell, S. Mitsch, and A. Platzer. Verified Quadratic Virtual Substitution for Real Arithmetic. Formal Methods (FM) 2021. (doi | arXiv | AFP)
K. Cordwell, Y. K. Tan, and A. Platzer. A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm. Interactive Theorem Proving (ITP) 2021. (pdf | doi | AFP)
A. Sogokon, S. Mitsch, Y. K. Tan, K. Cordwell, and A. Platzer. Pegasus: A Framework for Sound Continuous Invariant Generation. Formal Methods (FM) 2019. (pdf | doi).
This paper was awarded the FM Best Tool Paper Award.K. Cordwell and A. Platzer. Towards Physical Hybrid Systems. Conference on Automated Deduction (CADE) 2019. (pdf | doi | slides)
Journal Papers (note: authorship in math journals is alphabetical)
CS Journals
A. Sogokon, S. Mitsch, Y. K. Tan, K. Cordwell, and A. Platzer. Pegasus: Sound continuous invariant generation. Formal Methods in System Design (FMSD) 2021. (doi | arXiv)
Special issue for selected papers from FM'19.
Math JournalsP. Cohen, K. Cordwell, A. Epstein, C-H. Kwan, A. Lott, and S. J. Miller, On near-perfect numbers. Acta Arithmetica, 194 (2020), 341-366. (doi)
K. Cordwell, A. Epstein, A. Hemmady, S. J. Miller, E. Palsson, A. Sharma, S. Steinerberger, and Y. N. T. Vu, On algorithms to calculate integer complexity. Integers, 19 (2019). (pdf | arXiv)
K. Cordwell, M. Hlavacek, C. Huynh, S. J. Miller, C. Peterson, and Y. N. T. Vu, Summand minimality and asymptotic convergence of generalized Zeckendorf decompositions. Research in Number Theory, 4 (2018), no. 43. (pdf | doi)
K. Cordwell and G. Wang, Multilinear polynomials of small degree evaluated on matrices over a unital algebra. Linear Algebra and its Applications, 496 (2016), 262-287. (doi)
K. Cordwell, T. Fei, and K. Zhou, On lower central series quotients of finitely generated algebras over Z. Journal of Algebra, 423 (2015), 559-572. (doi | arXiv)
Book Chapters
Benedetto J.J., Cordwell K., Magsino M. (2019) CAZAC Sequences and Haagerup's Characterization of Cyclic N-roots. In: Aldroubi A., Cabrelli C., Jaffard S., Molter U. (eds) New Trends in Applied Harmonic Analysis, Volume 2. Applied and Numerical Harmonic Analysis. Birkhäuser, Cham. (doi)
PhD Thesis
Formally Verifying Algorithms for Real Quantifer Elimination (2023)
Committee: André Platzer (Chair), Jeremy Avigad, Frank Pfenning, Dexter Kozen, Lawrence Paulson
Document: Available here
Work Experience
I interned at NASA Langley Research Center with the Formal Methods group in the summer of 2019. Under the mentorship of Aaron Dutle and César Muñoz, I worked to improve quantifier elimination strategies in the PVS theorem prover; my contributions are now included in the NASA PVS library. The associated tech report is available here.
Fun Fact
I participated in science fairs and similar science competitions in high school and was fortunate to work with some fantastic mentors who were very generous with their time and talents. You can see me talk about some of my early (high school) research below!