BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:IC Colloquium : Directions to and for verified software
DTSTART:20170306T101500
DTEND:20170306T113000
DTSTAMP:20260407T230633Z
UID:023db47ff714fb72cc89172d28d9299a4ddbfc6a3d2a735b7879c357
CATEGORIES:Conferences - Seminars
DESCRIPTION:By : Rustan Leino - Microsoft Research\n\nAbstract :\nThere wi
 ll always be computer programs whose behavior doesn't have to meet any pa
 rticular expectations.  But there is an increasing number of computer sys
 tems whose correct functioning affects our society:  vehicular operation
 s\, secure transactions in web browsers\, storage of medical information\
 , digital currencies\, etc.  Luckily\, there has also been progress in so
 ftware development methods that can assist software engineers in producing
  verifiably correct software.\n \nIn this talk\, I will describe where re
 search in program verification has brought us today\, give a demo of a sta
 te-of-the-art system for writing verified programs\, and discuss direction
 s for what may be possible in the future.\n\nBio :\nRustan Leino is Princi
 pal Researcher in the Research in Software Engineering (RiSE) group at Mic
 rosoft Research\, Redmond and Visiting Professor in the Department of Comp
 uting 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 too
 ls Dafny\, Chalice\, Jennisys\, Spec#\, Boogie\, Houdini\, ESC/Java\, and 
 ESC/Modula-3.  He is an ACM Fellow.\nPrior 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 channel on youtube. He
  is a multi-instrumentalist\, he instructed group cardio and strength clas
 ses for many years\, and he likes to cook.\n\nMore information
LOCATION:BC 420 https://plan.epfl.ch/?room==BC%20420
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR