BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Well-founded functions\, induction\, and extreme predicates in an 
 SMT-based verifier - Rustan Leino\, Microsoft Research Redmond
DTSTART:20161201T100000Z
DTEND:20161201T110000Z
UID:TALK69504@talks.cam.ac.uk
CONTACT:44515
DESCRIPTION:An SMT solver takes first-order formulas as input and provides
  impressive automation.  But what if the problem at hand goes beyond first
  order?  The Dafny program verifier provides well-functions\, inductive pr
 oofs\, and predicates defined as least and greatest fixpoints.  It encodes
  properties of these into first-order logic in such a way that harnesses t
 he automation of SMT solvers.  In this talk\, I will give an overview of f
 unctions and induction in Dafny\, and will then focus on the encoding on p
 redicates defined by fixpoints.  I hope to learn more about fixpoints and 
 ordinal numbers as I do.\n\n
LOCATION:Auditorium\, Microsoft Research Ltd\, 21 Station Road\, Cambridge
 \, CB1 2FB
END:VEVENT
END:VCALENDAR