Eventi
29
Settembre
2022
29.
09.
2022
06
Ottobre
2022
06.
10.
2022
13
Ottobre
2022
13.
10.
2022
20
Ottobre
2022
20.
10.
2022
27
Ottobre
2022
27.
10.
2022
03
Novembre
2022
03.
11.
2022
10
Novembre
2022
10.
11.
2022

Informatics Seminar on Wednesday, December 3rd at 12.30 by K. Rustan M. Leino

Decanato - Facoltà di scienze informatiche

Data d'inizio: 3 Dicembre 2008

Data di fine: 4 Dicembre 2008

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)
 
TIME: 12.30
 
ABSTRACT:
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.
 
BIO:
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