I am a fourth year Ph.D. student in Carnegie Mellon University's Computer Science Department. I am advised by André Platzer and am part of the Logical Systems Lab. My interests include formal verification and ways in which math (especially algebra) and computer science intersect. Currently, I am interested in three different areas within the formal verification of cyber-physical systems (CPS): real arithmetic (especially quantifier elimination), efficient invariant generation, and modeling (specifically, how to write models of CPS that build in an awareness of physics into logic).

Before CMU, I was a math and cs major at the University of Maryland, College Park.

- M. Scharager,
**K. Cordwell**, S. Mitsch, and A. Platzer. Verified Quadratic Virtual Subsitution for Real Arithmetic.

Accepted to Formal Methods (FM) 2021, to appear. (arXiv) -
**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)

- 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. - P. 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 Yen Nhi Truong 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)

- 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)

- CMU: 15-424/624/824, Logical Foundations of Cyber-Physical Systems, Fall 2019
- UMD: CMSC250, Discrete Structures, Fall 2016 and Spring 2017

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.

- NSF GRFP Fellowship, 2017
- UMD Department of Mathematics Outstanding Senior Award, joint with Charles Parker, 2017
- Barry M. Goldwater Scholarship, 2016

- Sub-reviewed:
*Journal of Number Theory*, ITP 2018, CICM 2018, FASE 2019, CPP 2019, CADE 2019, LICS 2020 - Reviewed:
*Logical Methods in Computer Science* - Artifact Evaluation Committee: CAV 2020, CAV 2021

- TechNights: a CMU program aimed at introducing STEM concepts to middle school girls
- Fall 2019 - present: Co-coordinator
- Fall 2017 - Spring 2018: Led sessions on graph theory, logic games, cryptography, and dynamic programming
- During COVID-19, we have virtual sessions available here

- OurCS workshop 2019
- Science fair and science competitions (fun fact: I participated in science competitions in high school)
- College: Middle and High School Math Tutoring (MHSMT)

Email: kcordwel at cs.cmu.edu

Office: GHC 6002