Teaching Automata Theory and Formal Languages with Dafny
This talk describes a mandatory second-year undergraduate course on Automata Theory and Formal Languages for computer science and software engineering students, taught using the verification-aware programming language Dafny. The course closely follows Automata, Computability and Complexity: Theory and Applications by Elaine Rich. It covers finite state machines and regular expressions, pushdown automata and context-free grammars, ending with Turing machines and decidability. By encoding the formal definitions and key algorithms from this textbook in Dafny, a traditionally abstract mathematics course is transformed into an interactive, hands-on learning experience where students receive immediate feedback on both their machine constructions and their reasoning about formal languages. The course materials, leveraging Dafny’s unique combination of specification, verification, and code generation, have been made publicly available.
Dr. Ran Ettinger is a Senior Engineer at NVIDIA, developing tools and methodologies for the formal verification of software, combining bounded model checking with deductive verification for proving correctness of sequential and concurrent programs. Previously, as an adjunct lecturer at Ben-Gurion University of the Negev (BGU), in AFEKA – The Academic College of Engineering in Tel-Aviv, and in the Ramat Gan Academic College (RGAC), he was employing formal method techniques both in elective programming courses (at BGU and AFEKA, using Dafny and Ada/SPARK) and more recently in mandatory courses on the foundational subjects of Logic and Set Theory (at RGAC using Dafny) as well as Formal Languages and Automata Theory (at RGAC and AFEKA, using Dafny too). A passionate proof engineer and an experienced programmer with a history of research on static analysis of programs and on tools for software maintenance (IBM Research, Sun Microsystems Laboratories), Rani holds a Doctor of Philosophy degree from the University of Oxford (2008) and a Bachelor of Science degree in Mathematics and Computer Science from BGU (2000).
Sun 11 JanDisplayed 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 | ||
