Towards Physical Hybrid Systems. - Katherine Cordwell; André Platzer (CADE, 2019)

Pegasus: A Framework for Sound Continuous Invariant Generation. - Andrew Sogokon; Stefan Mitsch; Yong Kiam Tan; Katherine Cordwell; André Platzer (FM, 2019)

On Algorithms to Calculate Integer Complexity. - Katherine Cordwell; Alyssa Epstein; Anand Hemmandy; Steven J. Miller 001; Eyvindur A. Palsson; Aaditya Sharma; Stefan Steinerberger; Yen Nhi Truong Vu (Integers, 2019)

A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm. - Katherine Cordwell; Yong Kiam Tan; André Platzer (ITP, 2021)

The BKR Decision Procedure for Univariate Real Arithmetic. - Katherine Cordwell; Yong Kiam Tan; André Platzer (Arch. Formal Proofs, 2021)

Verified Quadratic Virtual Substitution for Real Arithmetic. - Matias Scharager; Katherine Cordwell; Stefan Mitsch; André Platzer (Arch. Formal Proofs, 2021)

Pegasus: sound continuous invariant generation. - Andrew Sogokon; Stefan Mitsch; Yong Kiam Tan; Katherine Cordwell; André Platzer (Formal Methods Syst. Des., 2021)

A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL. - Katherine Cordwell; Yong Kiam Tan; André Platzer (Arch. Formal Proofs, 2022)

Formalizing Pick's Theorem in Isabelle/HOL. - Sage Binder; Katherine Kosaian (CICM, 2024)

Formalizing Coppersmith's Method in Isabelle/HOL. - Katherine Kosaian; Yong Kiam Tan; Kristin Yvonne Rozier (CICM, 2024)

Pick's Theorem. - Sage Binder; Katherine Kosaian (Arch. Formal Proofs, 2024)

Formalizing Coppersmith's Method. - Katherine Kosaian; Yong Kiam Tan (Arch. Formal Proofs, 2024)

Babai's Nearest Plane Algorithm. - Eric Ren; Sage Binder; Katherine Kosaian (Arch. Formal Proofs, 2024)

Formalizing MLTL Formula Progression in Isabelle/HOL. - Katherine Kosaian; Zili Wang 004; Elizabeth Sloan; Kristin Y. Rozier (CoRR, 2024)

Language Partitioning for Mission-Time Linear Temporal Logic. - Alec Rosentrater; Zili Wang 004; Katherine Kosaian; Kristin Yvonne Rozier (NFM, 2025)

Formally Verifying a Transformation from MLTL Formulas to Regular Expressions. - Zili Wang 004; Katherine Kosaian; Kristin Yvonne Rozier (TACAS (1), 2025)

The Hidden Number Problem. - Sage Binder; Eric Ren; Katherine Kosaian (Arch. Formal Proofs, 2025)

Mission-time Linear Temporal Logic Formula Progression. - Katherine Kosaian; Zili Wang 004 (Arch. Formal Proofs, 2025)

Mission-time Linear Temporal Logic. - Katherine Kosaian; Zili Wang 004; Elizabeth Sloan (Arch. Formal Proofs, 2025)

Mission-time Linear Temporal Logic to Regular Expressions. - Zili Wang 004; Katherine Kosaian (Arch. Formal Proofs, 2025)

Language Partitioning for Mission-time Linear Temporal Logic. - Zili Wang 004; Katherine Kosaian; Alec Rosentrater (Arch. Formal Proofs, 2025)