Français Anglais
Accueil Annuaire Plan du site
Accueil > 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 décembre 2008

Le 15 janvier à 10h30 dans le grand amphi du PUIO, conférence exceptionnelle de 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:
Motion du LRI contre la LPPR
26 juin 2020

Ouvrage Informatique au lycée
18 juin 2020
Parution d'un ouvrage pour la spécialité NSI en classe de terminale, co-écrit par quatre membres du LRI.

Eugénie Brasier - 2ème prix MT180 PSaclay
07 avril 2020
Eugénie Brasier a eu le 2ème prix de Ma Thèse en 180 secondes de Paris-Saclay.