Dafny is a programming language designed to support verification. It grew roots in educational settings, was then used in systems research projects, and has now become a language used for industrial applications.

Throughout its many years as a workshop, FTfJP has explored the frontier of methodological issues related to programming in Java-like languages. Much of the focus has been on data structure with stateful objects. How do you write specifications for such data structures? How do you build formal verifiers for them?

In this lecture, I will talk about the state of Dafny and some of its recent applications. I will then review three common popular approaches to specifying stateful objects; among them, dynamic frames, which are used in Dafny. To show Dafny in action, I will show a simple stateful program that uses dynamic frames together with a new feature in Dafny, ghost constructors for algebraic datatypes.

K. Rustan M. Leino is Senior Principal Applied Scientist 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.