CS Colloquium
K.Rustan M. Leino, Microsoft Research
Title: The Dafny perspective on reasoning
Host: Ruzica Piskac
Abstract: Learning to reason about the correctness of software is important for every software engineer. In recent years, the availability of mechanical tools has brought reasoning back to the classroom. A goal of the research behind such tools is to make them usable by more programmers. As a step in that direction, Dafny is a programming language designed with reasoning in mind. In addition to common imperative and functional features, Dafny includes facilities for writing specifications and authoring proofs. Importantly, Dafny has an automated program verifier that runs in the IDE. This lets students use and experiment with important concepts like invariants and preconditions while sitting at the terminal authoring code. Dafny has also been used to teach mathematical induction and proofs, and to verify formal properties of language semantics, which previously was confined to more heavy-handed proof assistants.
Outside education, Dafny has been the primary language for the Ironclad Apps [OSDI 2014] and IronFleet [SOSP 2015] projects at Microsoft Research. All the code on these systems projects was written and verified not by formal-methods experts but by systems programmers.
In this talk, I will present Dafny and illustrate its use with some live demos.
Bio: Prof. Dr. K. Rustan M. Leino is a Principal Researcher in the Research in Software Engineering (RiSE) group at Microsoft Research, Redmond and a Visiting Professor in the Computing Department at Imperial College London. He is known for his work on programming methods, languages, and verification, and is a world leader in building automated program verification tools. Languages and tools he has worked on include Dafny, Chalice, Jennisys, Spec#, Boogie, Houdini, ESC/Java, and ESC/Modula-3. In the past, he has worked as a researcher at DEC and Compaq, and as a software engineer at Microsoft. He received his PhD in Computer Science from Caltech in 1995.