Tutorials
Tutorials on formal specification and verification, with examples drawn from my research.
All tutorials
-
Detecting redundant LTL requirements with Spot
Tutorial 24 min read
An introduction to LTL property refinement, with a Python example that checks implication and equivalence and identifies which requirements need separate verification.
- Read the tutorial: Detecting redundant LTL requirements with Spot
- Based on the FSE 2026 paper: Property Refinement in Linear Temporal Logic: Formal Semantics and Algorithms for Software Verification
- Paper DOI: Property Refinement in Linear Temporal Logic: Formal Semantics and Algorithms for Software Verification