🔥 Verification Hack and Learn: Tackling Mutable Objects in Dafny

### Join us for the next hands-on session of Verification Hack and Learn. We’ll dig into the practical challenges of verifying classes and mutable state in Dafny—and work together to overcome them.

What to Expect:

• Inspiration from the Article
  We’ll walk through the “Verified Ordered Set in Dafny” tutorial—exploring how an ordered set is specified, what invariants are needed, and where Dafny verification becomes challenging.
• Core Challenges with Mutable Objects
  Discussion will spotlight key hurdles:
• Maintaining class invariants and correct representation sets (`Repr`) when dealing with mutable fields.
• Managing reads and modifies framing—explicitly declaring what memory can be accessed or changed, and why it's vital for sound verification.
• Learning how loops and heap mutations can unintentionally invalidate invariants and cause verification failures.
• Live Dafny Exploration
  We’ll open a sample “ordered set” class and collaboratively:
• Identify necessary attributes and invariants.
• Tinker with `modifies` and `reads` clauses.
• Observe where Dafny balks—and why.
• Group Work & Debugging Practice
  In small groups, pick a simple Dafny class or mutable structure. Try:
• Adding invariants and framing.
• Testing how modifications and loops affect verification.
• Iteratively refining until the code verifies—or tracking why it doesn’t.
• Tips & Lessons Learned
  Wrap up with a group debrief:
• What patterns helped?
• What common pitfalls did we hit?