Dafny is a programming language designed to make reasoning possible and fun. It features standard imperative constructs like assignments, loops, and dynamically instantiable classes as well as functional constructs like datatypes, co-datatypes, and recursive functions. The language also features constructs for writing specifications and authoring proofs. The cross-platform development environments for Dafny continuously apply an automated program verifier to the programs being written, providing immediate feedback on the programs and proofs being authored.

Owing in part to its gentle learning curve and familiar programming feel, Dafny has been used in systems, security, and PL projects, in academia and industry, in verification competitions, and at several dozens of universities in teaching. Dafny can be used as an intelligent assistant in programming and modeling, and it can be used as a logical framework.

Now, Dafny comes to you in this 30-minute overview tutorial. Come see Dafny in action, learn how to use Dafny to reason about code, algorithms, and meta theory, and get inspired for how to apply or extend Dafny yourself.

K. Rustan M. Leino is Senior Principal Engineer in the Automated Reasoning Group at Amazon Web Services. He works on ways to make sure programs behave as intended, secure and functionally correct. Leino 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 been Principal Researcher at Microsoft Research, Visiting Professor at Imperial College London, and 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.