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: http://www.inria.fr/saclay/actualites/conf-rustan-leino
News
TrackML dans Nature
21 juin 2018
L'apprentissage automatique peut-il aider la physique des hautes énergies à découvrir et à caractériser de nouvelles particules ? TAO participe à l'organisation du challenge TrackML avec le CERN. La seconde phase de la compétition utilisera Codalab.

Un article de Isabelle Guyon sur la démocratisation de l'IA
19 mars 2018
Lien vers l'article paru dans le journal le monde :
http://www.lemonde.fr/acces-restreint/sciences/article/2018/04/08/a4544bd07cad09fe52980c0f82c08b34_5282548_1650684.html

Michèle Sebag a été élue membre de l'Academie des Technologies
13 avril 2018
Michèle Sebag, DR CNRS et Directrice Adjointe du LRI, a été élue membre de l'Academie des Technologies

https://www.academie-technologies.fr/members/454-michele-sebag