Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
Explore a 19-minute conference talk from the Dafny 2025 workshop where Stefan Zetzsche and Wojciech Różowski present their formal verification work on regular expressions. Learn how they use Dafny, a verification-aware programming language, to prove that the denotational (inductive) and operational (coinductive) semantics of regular expressions are equivalent up to pointwise bisimilarity. The presentation demonstrates how Dafny's inductive and coinductive features make it particularly well-suited for formalizing what was previously only established through proofs-by-hand. The speakers also provide interpretations in the language of Coalgebra throughout their formalization, suggesting their approach could serve as a blueprint for future generalizations to other theories. This talk was presented at the ACM SIGPLAN-sponsored Dafny 2025 workshop on January 19, 2025.
