I am a third 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.

- P. Cohen, K. Cordwell, A. Epstein, K. Kwan, A. Lott, and S. J. Miller, On Near Perfect Numbers, accepted to
*Acta Arithmetica*. (ArXiV) - 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)

In Fall 2019, I was a TA for CMU's 15-424/624/824, Logical Foundations of Cyber-Physical Systems.

I was a TA for UMD's CMSC250 (Discrete Structures) in Fall 2016 and Spring 2017.

I worked 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. Previously, PVS had three strategies for univariate quantifier elimination: `hutch`, `tarski`, and `sturm`. Of these, only `hutch` was able to work on arbitrary queries. I extended `tarski` to work on arbitrary queries by formalizing a DNF transformation. I also added preprocessing methods that exploit polynomial structure to `tarski`. These methods significantly improve the speed of `tarski` when they succeed and introduce no noticeable overhead when they fail.

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

Promoting the significance of the STEM sciences to younger students, especially from underrepresented groups, is important to me. In college, I first participated in and then helped to coordinate the Middle and High School Math Tutoring (MHSMT) program, a student-run organization that sent tutors to local high schools to assist students with their coursework in mathematics.

Currently, in graduate school, I volunteer for Tech Nights, which is a CMU program to teach middle school girls math and science concepts that they don't necessarily encounter in school. Most weeks, I assist with activities, but I have also co-led sessions on logic games, graph theory, cryptography, and dynamic programming.

I was very involved with science fair and similar competitions in high school. (See me talk about some of my work here!) I was fortunate to have the opportunity to volunteer at Intel ISEF 2018, held in Pittsburgh. Among other things, I served on a panel of science fair alumni. In 2017, I got to interact with Broadcom Masters finalists and answer their questions as part of a panel.

Email: kcordwel at cs.cmu.edu

Office: GHC 6002