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
- K. Cordwell, Y. K. Tan, and A. Platzer. A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm. Accepted to ITP 2021, to appear. (arXiv | AFP)
- A. Sogokon, S. Mitsch, Y. K. Tan, K. Cordwell, and A. Platzer. Pegasus: A Framework for Sound Continuous Invariant Generation. In Annabelle McIver and Maurice ter Beek, editors, FM 2019: Formal Methods - 23rd International Symposium, Porto, October 7-11, 2019, Proceedings, LNCS. Springer, 2019. © Springer (pdf | doi). This paper was awarded the FM Best Tool Paper Award.
- K. Cordwell and A. Platzer. Towards Physical Hybrid Systems. In Pascal Fontaine, editor, International Conference on Automated Deduction, CADE'19, Natal, Brazil, Proceedings, LNCS. Springer, 2019. © Springer-Verlag (pdf | doi | slides)
Journal Papers (note: authorship in math journals is alphabetical)
- A. Sogokon, S. Mitsch, Y. K. Tan, K. Cordwell, and A. Platzer. Pegasus: Sound continuous invariant generation. Formal Methods in System Design (2021). Special issue for selected papers from FM'19. © Springer (doi | arXiv)
- 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)
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
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