Katherine Kosaian is an Assistant Professor in Computer Science at the University of Iowa, where she is part of the Computational Logic Center.  Previously, she completed a one-year postdoc at Iowa State University. Her PhD is from Carnegie Mellon University's Computer Science Department. Her thesis, which won the 2024 Bill McCune PhD Award, was on formalizing algorithms for real quantifier elimination.

Research Interests

Her research interests include formal verification, interactive theorem proving, and ways in which math and computer science intersect. She is particularly interested in formalizing mathematics and algorithms with safety-critical applications.

Research Interests (Keywords)

Formal Verification; Interactive Theorem Proving; Mathematics

Selected Publications

• Formalizing Pick's Theorem in Isabelle/HOL. S. Binder and K. Kosaian. Conference on Intelligent Computer Mathematics (CICM) 2024.
• Formalizing Coppersmith's Method in Isabelle/HOL. K. Kosaian, Y. K. Tan, and K. Y. Rozier. Conference on Intelligent Computer Mathematics (CICM) 2024.
• A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL. K. Kosaian, Y. K. Tan, and A. Platzer. Certified Programs and Proofs (CPP) 2023.
• Verified Quadratic Virtual Substitution for Real Arithmetic. M. Scharager, K. Cordwell, S. Mitsch, and A. Platzer. Formal Methods (FM) 2021.
• A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm. K. Cordwell, Y. K. Tan, and A. Platzer. Interactive Theorem Proving (ITP) 2021.