Katherine Cordwell

About me

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.

Conference Papers

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 (authorship alphabetical)

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)

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

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.

Work Experience

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.

Awards

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

Outreach

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.

Contact

Email: kcordwel at cs.cmu.edu

Office: GHC 6002