The Design of an Interactive Proof Mode for Dafny

Ştefan Ciobâcă, K. Rustan M. Leino, Ştefan-Alexandru Mercaş +1

We propose to extend the Dafny system with an interactive proof mode. We present a motivating example, how the IPM works, including the main design choices we make, and a prototype…