This program is tentative and subject to change.
Using the Dafny verification system, we formally verify a range of minimax and negamax search algorithms, including variations with alpha-beta pruning and transposition tables. For depth-limited search with transposition tables, we introduce a witness-based correctness criterion and apply it to two representative algorithms. All verification artifacts, including proofs and Python implementations, are publicly available.
| Formal Verification of Minimax Algorithms (Formal Verification of Minimax Algorithms.pdf) | 493KiB |
This program is tentative and subject to change.
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 and Ben-Gurion University of the Negev and Israel Academic College in Ramat Gan | ||
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 | ||
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 | ||