BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Well-founded functions\, induction\, and extreme predicates in an 
 SMT-based verifier
DTSTART:20170308T093000
DTEND:20170308T103000
DTSTAMP:20260413T144001Z
UID:3a76a5274f23de65b6403917340dbd01a546895766ed4c862e6494b8
CATEGORIES:Conferences - Seminars
DESCRIPTION:by Rustan Leino\n\nAbstract\nAn SMT solver takes first-order f
 ormulas as input and provides impressive automation.  But what if the pro
 blem at hand goes beyond first order?  The Dafny program verifier provide
 s well-founded functions\, inductive proofs\, and predicates defined as le
 ast and greatest fixpoints.  It encodes properties of these into first-or
 der logic in such a way that harnesses the automation of SMT solvers.  In
  this talk\, I will give an overview of functions and induction in Dafny\,
  and will then focus on the encoding on predicates defined by fixpoints.\n
 \nBio\nRustan Leino is Principal Researcher in the Research in Software En
 gineering (RiSE) group at Microsoft Research\, Redmond and Visiting Profes
 sor in the Department of Computing at Imperial College London. He is known
  for his work on programming methods and program verification tools\, and 
 is a world leader in building automated program verification tools. These 
 include the languages and tools Dafny\, Chalice\, Jennisys\, Spec#\, Boogi
 e\, Houdini\, ESC/Java\, and ESC/Modula-3.  He is an ACM Fellow.\nPrior t
 o 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 c
 ollects thinking puzzles on a popular web page and hosts the Verification 
 Corner channel on youtube. In his spare time\, he likes to cook and\, bein
 g a multi-instrumentalist\, play music. Leino instructed group cardio and 
 strength classes for many years\, he more recently danced on a salsa perfo
 rmance team\, and he once needed a helicopter to get off a Swiss mountain.
 \n\nMore information\n 
LOCATION:BC 410 https://plan.epfl.ch/?room==BC%20410
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR