UTCS Colloquium - K. Rustan M. Leino/Microsoft Research, "Dafny: a program verifier for functional correctness, and for students", ACES 2.302

Contact Name: 
Jenna Whitney
Date: 
Jan 27, 2011 2:00pm - 3:00pm

There is a sign-up schedule for this event that can be found at

http://www.cs.utexas.edu/department/webevent/utcs/events/cgi/list_event

s.cgi

Type of Talk: UTCS Colloquia

Speaker/Affiliation: K. Rustan
M. Leino/Microsoft Research

Date/Time: January 27, 2011, 2:00 p.m.

Location: ACES 2.302

Host: Jay Misra & William Cook

Talk Tit

le: Dafny: a program verifier for functional correctness, and for students

Talk Abstract:
Dafny is a programming language and program verifie

r (research.microsoft.com/dafny). Based on an imperative, object-based lan

guage (some may say Pascal-like), Dafny incorporates some specification fe

atures that make it suitable for some kinds of functional-correctness verif

ications. The program verifier runs in the background as the program is be

ing designed and reports verification errors like other compiler errors. D

afny 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 V

erified Software Competition 2010. In this talk, I present Dafny through

a number of demos that showcase its features and user interaction.

Spe

aker Bio:
Rustan Leino is a Principal Researcher in the Research in Softw

are Engineering (RiSE) group at Microsoft Research. He is known for his wo

rk on programming methods and program verification tools. At Microsoft Res

earch, he has led the Spec# project, which brings enforced pre- and post-

conditions to the .NET platform, and is the architect of the Boogie progra

m verification framework, which underlies several program verifiers for Sp

ec#, 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 B

achelor''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 st

arted the Verification Corner video show on channel9.msdn.com. In his spar

e time, he plays music and teaches cardio exercise classes.