2 citations · 2 across the 5 of their papers we have counts for
5 papers
Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar
Sage Binder, Hanna Lachnitt, Katherine Kosaian
In Isabelle/HOL, declarative proofs written in the Isar language are widely appreciated for their readability and robustness. However, some users may prefer writing procedural "app…
Formally Verifying a Transformation from MLTL Formulas to Regular Expressions
Zili Wang, Katherine Kosaian, Kristin Yvonne Rozier
Mission-time Linear Temporal Logic (MLTL), a widely used subset of popular specification logics like STL and MTL, is often used to model and verify real world systems in safety-cri…
Formalizing MLTL Formula Progression in Isabelle/HOL
Katherine Kosaian, Zili Wang, Elizabeth Sloan +1
Mission-time Linear Temporal Logic (MLTL) is rapidly increasing in popularity as a specification logic, e.g., for runtime verification and model checking, driving a need for a trus…
Formalizing Pick's Theorem in Isabelle/HOL
Sage Binder, Katherine Kosaian
We formalize Pick's theorem for finding the area of a simple polygon whose vertices are integral lattice points. We are inspired by John Harrison's formalization of Pick's theorem…
A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
Katherine Kosaian, Yong Kiam Tan, André Platzer
We formalize a multivariate quantifier elimination (QE) algorithm in the theorem prover Isabelle/HOL. Our algorithm is complete, in that it is able to reduce any quantified formula…