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.
Thesis
My thesis will be about formally verifying algorithms for real quantifier elimination. The proposal is available here.
Conference Papers
- M. Scharager, K. Cordwell, S. Mitsch, and A. Platzer. Verified Quadratic Virtual Subsitution for Real Arithmetic.
Formal Methods (FM) 2021. (doi | arXiv | AFP) - 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 Y. N. T. 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 and 15-317/657, Constructive Logic, Fall 2021
- 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 - Fall 2021: Co-coordinator
- Fall 2017 - Spring 2018: Led sessions on graph theory, logic games, cryptography, and dynamic programming
- During COVID-19, we had virtual sessions, which are available here and 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