POPL 2026 (series) / Dafny 2026 (series) / Dafny 2026 /
Explicit Abstraction Barrier for Autoactive Verification
Sun 11 Jan 2026 11:18 - 11:36 at Horizons - Development of Auto-Active Verifiers
Coma is a verification language that allows the programmer to decide which part of a function implementation is visible to (and verified by) the caller, and which part is hidden from the caller and verified at the definition site. In this paper, we show through a series of examples how this functionality allows for extra flexibility, leading to more concise and natural specifications—if we write them at all.
Sun 11 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
Sun 11 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change
11:00 - 12:30 | |||
11:00 18mTalk | Diagnostics in Probabilistic Program Verification Dafny Philipp Schröer RWTH Aachen University, Darion Haase RWTH Aachen University, Joost-Pieter Katoen RWTH Aachen University | ||
11:18 18mTalk | Explicit Abstraction Barrier for Autoactive Verification Dafny Paul Patault Université Paris-Saclay - Laboratoire de Méthodes Formelles Pre-print | ||
11:36 18mTalk | Managing the Proof Context in SPARK Dafny File Attached | ||
11:54 18mTalk | Tunable Automation in Automated Program Verification Dafny Alexander Bai New York University, Chris Hawblitzel Microsoft Research, Andrea Lattuada VMware Research Pre-print | ||
12:12 18mTalk | Velvet: A Multi-Modal Verifier for Effectful Programs Dafny Vladimir Gladshtein , George Pîrlea National University of Singapore, Qiyuan Zhao National University of Singapore, Vitaly Kurin Neapolis University Pafos, Ilya Sergey National University of Singapore Pre-print | ||