Katherine Cordwell
About me
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.
Conference Papers
- 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)
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. - 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)
Math Journals
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)
Teaching
- CMU: 15-424/624/824, Logical Foundations of Cyber-Physical Systems, Fall 2019
- UMD: CMSC250, Discrete Structures, Fall 2016 and Spring 2017
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.
Awards
- NSF GRFP Fellowship, 2017
- UMD Department of Mathematics Outstanding Senior Award, joint with Charles Parker, 2017
- Barry M. Goldwater Scholarship, 2016
Reviews
- 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
Outreach
- 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)
Contact
Email: kcordwel at cs.cmu.edu
Office: GHC 6002