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: http://www.inria.fr/saclay/actualites/conf-rustan-leino