4 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…
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…
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 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…