The Faculty of Informatics is pleased to announce a seminar given by K. Rustan M. Leino
TITLE: Specification techniques for verifying object-oriented software
SPEAKER: K. Rustan M. Leino, Microsoft Research, Redmond
DATE: Wednesday, December 3rd, 2008
PLACE: USI Università della Svizzera italiana, room SI-004, Informatics building (Via G. Buffi 13)
To formally verify object-oriented programs, one needs program specifications and a program verifier. While some of the program verifier technology is by now well understood, the last 10 years have brought about several specification techniques. In this talk, I will compare three styles of specifications: the "Boogie methodology" used in Spec#, the "dynamic frames" used in the experimental language Dafny, and the "permission model" used in the experimental concurrent language Chalice. I will also include small demos of these three verification systems, which have been developed at Microsoft Research.
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. At Microsoft Research, he has led the Spec# project, which brings enforced pre- and postconditions to the .NET platform, and is the architect of the Boogie program verification framework, which underlies several program verifiers for Spec#, C, and other languages. Previously, Leino led the ESC/Java project at Compaq SRC, and worked on specifications on the pioneering ESC/Modula-3 project at DEC SRC. Before getting his PhD (Caltech, 1995), Leino wrote and designed object-oriented software as a technical lead in the Windows NT group at Microsoft. In his spare time, he plays music and teaches cardio exercise classes.
HOST: Prof. Natasha Sharygina