[PRL] Fwd: [MIT-PL] TALK:Monday 6-4-12 PL Seminar: Dafny: a tool for program correctness

[David Van Horn]

This was a cool talk at NEPLS...  -- David


-------- Original Message --------
Subject: [MIT-PL] TALK:Monday 6-4-12 PL Seminar: Dafny: a tool for 
program correctness
Date: Mon, 04 Jun 2012 00:01:03 -0400
From: Csail Event Calendar <eventcalendar at csail.mit.edu>
To: pl at lists.csail.mit.edu


PL Seminar: Dafny: a tool for program correctness
Speaker: K. Rustan M. Leino
Speaker Affiliation: Microsoft Research
Host: Adam Chlipala
Host Affiliation: CSAIL

Date: 6-4-2012
Time: 4:00 PM - 5:30 PM
Location: 32-D463 (Star)

Abstract:

Dafny is a programming language and program verifier.  The language is
type-safe and sequential, and it includes common imperative features, 
dynamic
object allocation, and inductive datatypes.  In addition, the language has
built-in specification constructs, which let a programmer record the 
intended
behavior of the program.  Dafny's state-of-the-art SMT-based static program
verifier, which is run continuously in the background as the program is 
being
developed, enforces the consistency of a program and its specifications. 
  Some
may see Dafny as a modern incarnation of the vision encompassed by 
Euclid and
other pioneering program-correctness efforts.

Dafny has been used to verify a number of challenging algorithms.  It is 
also
being used in teaching, and the web version of the tool recently passed
100,000 submitted program-verification attempts.  Dafny
was a popular choice in the VSTTE 2012 program verification competition, and
two of those teams received medals.  Dafny's open-source implementation, 
which
builds on the program verification engine Boogie, has also been used as a
foundation for other verification tools.

In this talk, I will give an overview of Dafny and a taste of how to use
Dafny for program verification, including some advanced features like
induction.

URLs:

Dafny homepage:  http://research.microsoft.com/dafny
Try Dafny on the web:  http://www.rise4fun.com/Dafny

Speaker:

K. Rustan M. Leino
Microsoft Research

Bio:

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.  These include the
languages and tools Dafny, Chalice, Jennisys, Spec#, Boogie, Houdini,
ESC/Java, and ESC/Modula-3.

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 video show on channel9.msdn.com.  In his spare time, he plays music
and, recently having ended his tenure as cardio exercise class 
instructor, is
trying to learn to dance.

Relevant URL(S): http://research.microsoft.com/dafny
For more information please contact: Adam Chlipala, adamc at csail.mit.edu

_______________________________________________
Pl mailing list
Pl at lists.csail.mit.edu
https://lists.csail.mit.edu/mailman/listinfo/pl
http://projects.csail.mit.edu/pl