CSD Graduate Katherine Kosaian Receives 2024 Bill McCune PhD Award

Breakthrough in the testing of cyber-physical systems

Thursday, July 11, 2024 - by Jenn Landefeld

Award winner Katherine Kosaian with PhD advisor André Platzer (left) and Carsten Fuhs. Kosaian received the Bill McCune PhD Award presented at IJCAR 2024, the 12th International Joint Conference on Automated Reasoning held July 1-6, 2024 in Nancy, France. (Photo: Jürgen Giesl)

Katherine Kosaian, formerly Cordwell, who received her doctoral degree from the Computer Science Department at Carnegie Mellon University, has been selected as the 2024 recipient of the Bill McCune PhD Award. Her dissertation, Formally Verifying Algorithms for Real Quantifier Elimination, was chosen for its strong theoretical and practical contributions to formally verified quantifier elimination for the first-order logic of real arithmetic. The award was presented at the 12th International Joint Conference on Automated Reasoning (IJCAR 2024) held July 1-6, 2024 in Nancy, France.

Kosaian’s advisor, André Platzer, Alexander von Humboldt Professor for Logic of Autonomous Dynamical Systems at Karlsruhe Institute of Technology, formerly Professor of Computer Science at Carnegie Mellon, notes that her research achieves a combination of formally verified algorithms for the real arithmetic decision problem and quantifier elimination problem that is efficient and competitive in practice for important fragments and yet is universal in solving the full problem. The approach she is following is on the path to a sophisticated algorithm with good parallel computational complexity bounds.

Her thesis formalizes virtual substitution as an incomplete yet practically relevant quantifier elimination technique and provides a verified executable implementation via code generation that is experimentally competitive with unverified state-of-the-art implementations. In addition to virtual substitution, her thesis also considers complete quantifier elimination algorithms. In particular, it provides the first quantifier elimination algorithm for the full multivariate setting that is formally verified in the theorem prover Isabelle/HOL, an important step towards the verification of the more optimized state-of-the-art algorithms.

Kosaian’s leading research in this area contributes significantly to the scientifically deep and technical field of real arithmetic decision procedures where the outcomes have to actually be correct because they matter as, for example, they are used to analyze the safety of cyber-physical systems that integrate sensing, computation, control and networking into physical objects and infrastructure, connecting them to the Internet and to each other. 

"Katherine Kosaian's work is a significant advance in formal verification and provides new tools and methods that help to develop safer and more reliable cyber-physical systems and robot motion planning," explains Professor Platzer.

After a postdoctoral year at Iowa State University, Kosaian will be starting in fall 2024 as an assistant professor in the Department of Computer Science at the University of Iowa, where she will be part of the Computational Logic Center.

About the Award:

In 2019 The International Conference on Automated Deduction (CADE, Inc.) established the Bill McCune PhD Award to annually recognize a PhD thesis defended the previous year, for its substantive contributions to the field of Automated Reasoning, its theory, its implementation, and/or its application on important problems. The award is named after the American computer scientist William Walker McCune, best known for the development of the Otter, Prover9, and Mace4 automated reasoning systems, and the automated proof of the Robbins conjecture using the EQP theorem prover.

Media Contact:

Jenn Landefeld | jennsbl@cs.cmu.edu