Verification Hack and Learn: Modular Data Structures in Dafny (ADT Verification)

This session dives into the world of modular data structure verification using Dafny, inspired by the work presented in "Verification of mutable linear data structures and iterator-based algorithms in Dafny" by Jorge Blázquez, Manuel Montenegro, and Clara Segura. We'll be exploring code from their accompanying GitHub repository: https://github.com/jorge-jbs/adt-verification-dafny .
This meetup is ideal for those wanting to level up their Dafny skills and understand how to build reusable, verifiable components. We'll cover:

• Modular Design: How to structure Dafny code using modules for better organization and reusability.
• Abstract Data Types (ADTs): Implementing mutable data structures like stacks, queues, and lists with iterators in a safe and verifiable way.
• Iterator Invalidation: Understanding and verifying how modifications to the underlying data structure affect iterator validity – a common source of bugs!
• Code Reuse & Boilerplate Reduction: Techniques for extracting common verification patterns and reducing repetitive code.

Resources:

• Paper: https://www.sciencedirect.com/science/article/pii/S2352220823000299
• GitHub Repository: https://github.com/jorge-jbs/adt-verification-dafny

All levels are welcome – whether you're new to Dafny or looking for advanced techniques.