The Design of an Interactive Proof Mode for Dafny
\c{S}tefan Ciob\^ac\u{a}, K. Rustan M. Leino, \c{S}tefan-Alexandru Merca\c{s}, Roxana-Mihaela Timon
TL;DR
This paper introduces an interactive proof mode for the Dafny system, detailing its design, implementation, and how it enhances formal verification processes.
Contribution
It presents the design and prototype of an interactive proof mode for Dafny, a novel feature not previously available.
Findings
Prototype implementation demonstrates feasibility
Design choices improve user interaction
Enhances Dafny's verification capabilities
Abstract
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 implementation.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Polynomial and algebraic computation · Cryptography and Residue Arithmetic