Quantifiers meet their match(ing loop)

Опубликовано 7 июля 2016, 23:06

Quantifiers meet their match(ing loop): new techniques and tools for dealing with unpredictable performance in Dafny
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.