Saved in:
Bibliographic Details
Main Authors: Ciobâcă, Ştefan, Leino, K. Rustan M., Mercaş, Ştefan-Alexandru, Timon, Roxana-Mihaela
Format: Preprint
Published: 2025
Subjects:
Online Access:https://arxiv.org/abs/2512.20486
Tags: Add Tag
No Tags, Be the first to tag this record!
Table of Contents:
  • 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.