On January 26, join the CS department for "Using Dafny to reason about concurrency" presented by K. Rustan M. Leino, Microsoft Research.

ABSTRACT:
Dafny is a programming language and verification system primarily aimed at writing provably correct sequential programs.  The expressivity of the Dafny language and the automation of its verifier also make Dafny suitable for more general reasoning tasks, along the lines of a general proof assistant.  In this talk, I will present Dafny in its traditional setting. Then, I will use Dafny to model and prove correct the behavior of a concurrent algorithm.  The style is inspired by UNITY, TLA+, and Event-B, to which Dafny adds automated reasoning.

SPEAKER’S BIO:
Rustan Leino is Principal Researcher in the Research in Software Engineering (RiSE) group at Microsoft Research, Redmond and Visiting Professor in the Department of Computing at Imperial College London. 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. 
Prior to Microsoft Research, Leino worked 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 collects thinking puzzles on a popular web page and hosts the Verification Corner channel on youtube. In his spare time, he plays music and likes to cook.

The talk is taking place at 11:30a in Room 120 of the New Computer Science building. CSE students should sign in.