Katherine Kosaian (née Cordwell)

About me

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


My thesis will be about formally verifying algorithms for real quantifier elimination. The proposal is available here.

Conference Papers

  1. M. Scharager, K. Cordwell, S. Mitsch, and A. Platzer. Verified Quadratic Virtual Subsitution for Real Arithmetic.
    Formal Methods (FM) 2021. (doi | arXiv | AFP)
  2. 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)
  3. 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.
  4. 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
  1. 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.

  2. Math Journals
  3. 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)
  4. 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)
  5. 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)
  6. 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)
  7. 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


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.





Email: kcordwel at cs.cmu.edu

Office: GHC 6002