The Design of an Interactive Proof Mode for Dafny (Dafny 2026)

Sun 11 - Sat 17 January 2026 Rennes, France

Who

Ștefan Ciobâcă, K. Rustan M. Leino, Ștefan Mercaș, Roxana-Mihaela Timon

Track

Dafny 2026

Time Zone

The program is currently displayed in (GMT+01:00) Brussels, Copenhagen, Madrid, Paris.

Use conference time zone: (GMT+01:00) Brussels, Copenhagen, Madrid, ParisSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

When

Sun 11 Jan 2026 10:12 - 10:30 at Horizons - Keynote

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.

Ștefan Ciobâcă

Alexandru Ioan Cuza University of Iasi

Romania

K. Rustan M. Leino

Amazon

United States

Ștefan Mercaș

Alexandru Ioan Cuza University, Iasi, Romania

Roxana-Mihaela Timon