Title: Verified programs and proofs in Dafny
Speaker: K. Rustan M. Leino (Amazon)
Dates: October, 17 th, 18 th & 19 th ,
Where: Faculty of Informatics, Laboratorio E6 (UPV/EHU)
Organizers: Grupo LoRea & UFI Bailab
In this 3-day course, you will learn and practice the foundations of program verification, like pre- and postcondition specifications, loop invariants, termination, proofs, and induction. The Dafny programming language will be used throughout. In addition to imperative and functional programming features, the Dafny language includes specifications and
proof-authoring features. Roughly, the three half-days will focus on imperative programs and loop invariants, functional programming
and inductive proofs, and an overview of advanced topics like working with the heap.
The class will use hands-on exercises with Dafny throughout. The class setting will provide computers with Dafny installed. If you prefer, you can bring your own laptop with Dafny installed (Dafny installs in Visual Studio, emacs, and VS Code, see https://github.com/Microsoft/dafny).
K. Rustan M. Leino is Senior Principal Engineer in the Automated Reasoning Group at Amazon Web Services. He is known for his work
on programming methods and program verification tools, and is a world leader in building automated program verification tools. These
include the languages and tools Dafny, Chalice, Jennisys, Spec#, Boogie, Houdini, ESC/Java, and ESC/Modula-3.
He is an ACM Fellow.
Before Amazon, Leino has worked as Principal Researcher at Microsoft Research, a Visiting Professor at Imperial College London, and a
researcher at DEC/Compaq SRC. He received his PhD from Caltech (1995), before which he designed and wrote object-oriented software
as a technical lead in the Windows NT group at Microsoft. Leino hosts the Verification Corner channel on youtube. He is a multi-
instrumentalist, he instructed group cardio and strength classes for many years, and he likes to cook.