POPL 2026 (series) / Dafny 2026 (series) / Dafny 2026 /
Verification of E-Voting Algorithms in Dafny
Sun 11 Jan 2026 14:54 - 15:12 at Horizons - Applications and Lessons Learned
Electronic voting procedures are implementations of electoral systems, making it possible to conduct polls or elections with the help of computers. This paper reports on the development of an open-source library of electronic voting procedures, which currently covers Score Voting, Instant-Runoff Voting, Borda Count, and Single Transferable Vote. The four procedures, of which two are discussed in detail, have been implemented in Dafny, formally verifying the consistency with functional specifications and key correctness properties. Using code extraction from the Dafny implementation, the library has been used to set up a voting web service.
Sun 11 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
Sun 11 Jan
Displayed time zone: Brussels, Copenhagen, Madrid, Paris change
14:00 - 15:30 | |||
14:00 18mTalk | Lessons from Building an Auto-Active Verifier in Lean Dafny George Pîrlea National University of Singapore, Vladimir Gladshtein , Qiyuan Zhao National University of Singapore, Ilya Sergey National University of Singapore Pre-print | ||
14:18 18mTalk | Formal Verification of Minimax Algorithms Dafny Wieger Wesselink Eindhoven University of Technology, Kees Huizing Eindhoven University of Technology, Huub van de Wetering Eindhoven University of Technology File Attached | ||
14:36 18mTalk | Teaching Automata Theory and Formal Languages with Dafny Dafny Ran Ettinger NVIDIA Pre-print | ||
14:54 18mTalk | Verification of E-Voting Algorithms in Dafny Dafny Robert Büttner University of Regensburg, Fabian Franz Dießl University of Regensburg, Patrick Janoschek University of Regensburg, Ivana Kostadinovic University of Regensburg, Henrik Oback University of Regensburg, Kilian Voß University of Regensburg, Franziska Alber University of Regensburg, Roland Herrmann University of Regensburg, Sibylle Möhle University of Regensburg, Philipp Rümmer University of Regensburg and Uppsala University Pre-print | ||
15:12 18mTalk | A Correct-by-Construction Checker for Validation of Railway Data Dafny Benoît Boyer Mitsubishi Electric R&D Centre Europe, Rennes, France, Noé Canva Inria Saclay & Université Paris-Saclay, Matteo Manighetti IRIF, Université Paris Cité, Claude Marché Inria Saclay & Université Paris-Saclay Link to publication | ||