Katherine Kosaian

According to our database, Katherine Kosaian authored at least 23 papers between 2019 and 2026.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of three.

2026

Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar.

Sage Binder, Hanna Lachnitt, Katherine Kosaian

CoRR, March, 2026

2025

Language Partitioning for Mission-time Linear Temporal Logic.

Zili Wang, Katherine Kosaian, Alec Rosentrater

Arch. Formal Proofs, 2025

Mission-time Linear Temporal Logic to Regular Expressions.

Zili Wang, Katherine Kosaian

Arch. Formal Proofs, 2025

Mission-time Linear Temporal Logic.

Katherine Kosaian, Zili Wang, Elizabeth Sloan

Arch. Formal Proofs, 2025

Mission-time Linear Temporal Logic Formula Progression.

Katherine Kosaian, Zili Wang

Arch. Formal Proofs, 2025

The Hidden Number Problem.

Sage Binder, Eric Ren, Katherine Kosaian

Arch. Formal Proofs, 2025

Formally Verifying a Transformation from MLTL Formulas to Regular Expressions.

Zili Wang, Katherine Kosaian, Kristin Yvonne Rozier

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2025

Language Partitioning for Mission-Time Linear Temporal Logic.

Alec Rosentrater, Zili Wang, Katherine Kosaian, Kristin Yvonne Rozier

Proceedings of the NASA Formal Methods - 17th International Symposium, 2025

Formalizing MLTL Formula Progression in Isabelle/HOL.

Katherine Kosaian, Zili Wang, Elizabeth Sloan, Kristin Yvonne Rozier

Proceedings of the Intelligent Computer Mathematics - 18th International Conference, 2025

Formalizing the Hidden Number Problem in Isabelle/HOL.

Sage Binder, Eric Ren, Katherine Kosaian

Proceedings of the 16th International Conference on Interactive Theorem Proving, 2025

2024

Babai's Nearest Plane Algorithm.

Eric Ren, Sage Binder, Katherine Kosaian

Arch. Formal Proofs, 2024

Formalizing Coppersmith's Method.

Katherine Kosaian, Yong Kiam Tan

Arch. Formal Proofs, 2024

Pick's Theorem.

Sage Binder, Katherine Kosaian

Arch. Formal Proofs, 2024

Formalizing Coppersmith's Method in Isabelle/HOL.

Katherine Kosaian, Yong Kiam Tan, Kristin Yvonne Rozier

Proceedings of the Intelligent Computer Mathematics - 17th International Conference, 2024

Formalizing Pick's Theorem in Isabelle/HOL.

Sage Binder, Katherine Kosaian

Proceedings of the Intelligent Computer Mathematics - 17th International Conference, 2024

2023

A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL.

Katherine Kosaian, Yong Kiam Tan, André Platzer

Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2023

2021

Pegasus: sound continuous invariant generation.

Andrew Sogokon, Stefan Mitsch, Yong Kiam Tan, Katherine Cordwell, André Platzer

Formal Methods Syst. Des., 2021

The BKR Decision Procedure for Univariate Real Arithmetic.

Katherine Cordwell, Yong Kiam Tan, André Platzer

Arch. Formal Proofs, 2021

A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm.

Katherine Cordwell, Yong Kiam Tan, André Platzer

Proceedings of the 12th International Conference on Interactive Theorem Proving, 2021

Verified Quadratic Virtual Substitution for Real Arithmetic.

Matias Scharager, Katherine Cordwell, Stefan Mitsch, André Platzer

Proceedings of the Formal Methods - 24th International Symposium, 2021

2019

On Algorithms to Calculate Integer Complexity.

Katherine Cordwell, Alyssa Epstein, Anand Hemmandy, Steven J. Miller, Eyvindur A. Palsson, Aaditya Sharma, Stefan Steinerberger, Yen Nhi Truong Vu

Integers, 2019

Pegasus: A Framework for Sound Continuous Invariant Generation.

Andrew Sogokon, Stefan Mitsch, Yong Kiam Tan, Katherine Cordwell, André Platzer

Proceedings of the Formal Methods - The Next 30 Years - Third World Congress, 2019

Towards Physical Hybrid Systems.

Katherine Cordwell, André Platzer

Proceedings of the Automated Deduction - CADE 27, 2019