POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Sun 14 Jan 2024 14:36 - 14:54 at Turing Lecture - Proof Stability / Brittleness / Scale Chair(s): Stefan Zetzsche

Highly automated theorem provers like Dafny allow users to prove simple properties with little effort, making it easy to quickly sketch proofs.

The drawback is that such provers leave users with little control about the proof search, meaning that the small changes inherent to the iterative process of writing a proof often lead to unpredictable variations in verification time, and eventually hard-to-diagnose proof failures.

This sometimes turns the boon of high automation into a curse, as instead of breaking early and showing unsolved goals to the user like in Coq, proofs tend to gradually become unstable until their verification time explodes. At this point, the absence of a proof context to investigate often leaves the user to a painful debugging session.

In this paper, we show how to use Dafny modules to encode Coq-like induction principles to dramatically improve the stability and maintainability of proofs about inductive data structures.

Sun 14 Jan

Displayed time zone: London change

14:00 - 15:30
Proof Stability / Brittleness / ScaleDafny at Turing Lecture
Chair(s): Stefan Zetzsche Amazon Web Services
14:00
18m
Talk
Enhancing Proof Stability
Dafny
Sean McLaughlin Amazon Web Services, Georges-Axel Jaloyan Amazon Web Services, Tongtong Xiang Amazon Web Services, Florian Rabe Amazon Web Services
14:18
18m
Talk
Improving the Stability of Type Safety Proofs in Dafny
Dafny
Joseph W. Cutler University of Pennsylvania, Michael Hicks Amazon Web Services and the University of Maryland, Emina Torlak Amazon Web Services, USA
14:36
18m
Talk
Incremental Proof Development in Dafny with Module-Based Induction
Dafny
14:54
18m
Talk
Portfolio Solving for Dafny
Dafny
Eric Mugnier University of California San Diego, Sean McLaughlin Amazon Web Services, Aaron Tomb Amazon Web Services
15:12
18m
Talk
Domesticating Automation
Dafny
Pranav Srinivasan University of Michigan / VMware Research, Oded Padon VMware Research, Jon Howell VMware Research, Andrea Lattuada VMware Research