BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Developing verified programs in Dafny - Rustan Leino
DTSTART:20120227T124500Z
DTEND:20120227T140000Z
UID:TALK36333@talks.cam.ac.uk
CONTACT:Peter Sewell
DESCRIPTION:"Dafny":http://research.microsoft.com/dafny is a programming l
 anguage and program verifier. The language is sequential and includes comm
 on imperative features\, dynamic object allocation\, and inductive datatyp
 es. It also includes specification constructs like pre- and postconditions
 . Because the Dafny verifier runs continuously in the background\, the con
 sistency of a program and its specifications is always enforced.\n\nDafny 
 has been used to verify a number of challenging algorithms\, including Sch
 orr-Waite graph marking\, Floyd's "tortoise and hare" cycle-detection algo
 rithm\, and snapshotable trees with iterators. Dafny is also being used in
  teaching and it was a popular choice in the VSTTE 2012 program verificati
 on competition (where two of the Dafny teams received medals). Its open-so
 urce implementation (which rests on Boogie and makes use of the SMT solver
  Z3) has also been used as a foundation for other verification tools.\n\nI
 n this talk\, I will give a taste of how to use Dafny to write correct cod
 e.  In addition to showing the basic interaction with Dafny (which is done
  via the program text)\, I will show how to debug verification attempts an
 d how to formulate and prove (often inductive) lemmas.
LOCATION:FW26
END:VEVENT
END:VCALENDAR