Quantifiers meet their match(ing loop): new techniques and tools for dealing with unpredictable performance in Dafny

September 8, 2015
Clement Pit-Claudel | Microsoft Research

Large developments using the Dafny program verifier often suffer from the so-called butterfly effect, where minor modifications to the program source cause verification failures or large variations in verification times. This low predictability, made worse by the lack of high-level tools for debugging these issues, significantly degrades the experience of our users. This talk will describe my joint efforts with Rustan Leino to improve this development experience: I will discuss our Dafny-level implementation of trigger selection, trigger splitting, and matching-loop detection for user-written quantifiers, and demo new graphical performance debugging tools for z3. I will also briefly demo our new Emacs modes for Dafny and Boogie, and show how we connect IDEs with Dafny to encourage users to write z3-friendly quantifiers.

Speaker Details

Clément is a grad student at MIT, working in Adam Chlipala’s lab to create tools to make software more reliable. His research focuses on proof assistants, compilers, and programming languages, and his broader interests include databases, optimization, type theory, and linguistics.