Français Anglais
Accueil Annuaire Plan du site
Home > News du laboratoire > Séminaire Digiteo : K. Rustan M. Leino
Séminaire Digiteo : K. Rustan M. Leino
Séminaire Digiteo : K. Rustan M. Leino Séminaire Digiteo : K. Rustan M. Leino
15 December 2008

OnJanuary 15th at 10am30 in the PUIO amphitheater, seminar by Rustan Leino : "Verification tools at Microsoft"

Séminaire Digiteo co-organisé par l'INRIA et le LRI.

Le 15 janvier 2009 à 10h30, grand amphi du PUIO, bât 640, Université Paris-Sud.

Conférence de K. Rustan M. Leino : "Verification tools at Microsoft"

Abstract: Program verification and other symbolic-execution and static-analysis techniques are being explored and applied to software at Microsoft. In this talk, I will first describe and give a demo of Spec#, an experimental programming system that incorporates code contracts (like pre- and postconditions and invariants) and provides run-time checking and static verification of these code contracts. I will then give an overview of some other tools developed at Microsoft Research and applied to production software.

Short Biography: 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.

Pour en savoir plus:
Yannis Manoussakis passed away
6 June 2021
We have just learned of the death of Yannis Manoussakis, Professor at the University of Paris-Saclay, on Saturday June 5.

He was the leader of the GALaC team and had been for many years director of the LRI, we lose a friend and a dear colleague.


Semaine du cerveau : Cerveau connecté
16 March 2021

Wizard project
1 April 2021
Innovation Area: Public Safety, IoT, Mobility