Faculty Colloq & CSE 600: Using Dafny to reason about concurrency

Dates: 
Thursday, January 26, 2017 - 11:30 to 13:00
Location: 
Room 120 (105 Seats)

Faculty Colloquium Using Dafny to reason about concurrency

SPEAKER: 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.

Computed Event Type: 
Mis
Event Title: 
Faculty Colloq & CSE 600: Using Dafny to reason about concurrency