Seminars at the Faculty of Informatics

SPEAKER: Dr. Rustan Leino
DATE: Thursday, February 24th, 2011
PLACE: USI Università della Svizzera italiana, room A33, Red building (Via G. Buffi 13)
TIME: 13.30

Dafny is a programming language and program verifier (  Based on an imperative, object-based language (some may say Pascal-like), Dafny incorporates some specification features that make it suitable for some kinds of functional-correctness verifications.  The program verifier runs in the background as the program is being designed and reports verification errors like other compiler errors.  Dafny has been used to prove a number of challenging algorithms (like Schorr-Waite graph-marking), has been used in teaching, and fared well at the Verified Software Competition 2010.  In this talk, I present Dafny through a number of demos that showcase its features and user interaction.

Rustan Leino is a Principal Researcher in the Research in Software Engineering (RiSE) group at Microsoft Research.  He is known for his work on programming methods and program verification tools.  At Microsoft Research, he has led the Spec# project, which brings enforced pre- and post-conditions to the .NET platform, and is the architect of the Boogie program verification framework, which underlies several program verifiers for Spec#, C, and other languages.  Previously, Leino led the ESC/Java project at Compaq SRC and worked on specifications on the pioneering ESC/Modula-3 project at DEC SRC.
Leino received his PhD at Caltech (1995) and his Bachelor's at UT Austin (1989).  In between, he wrote and designed object-oriented software as a technical lead in the Windows NT group at Microsoft.  Leino collects thinking puzzles on a popular web page and has recently started the Verification Corner video show on  In his spare time, he plays music and teaches cardio exercise classes.

 HOST: Prof. Natasha Sharygina


URL 1: