Accueil/ expose
Comment faire confiance à un compilateur ?
jeudi 13 mars 2014

Loading the player...
Descriptif

Conférence de Xavier Leroy dans le cadre du Séminaire général du département d’informatique

Le logiciel critique - celui dont dépendent des vies humaines - nécessite des techniques de développement et de validation très particulières pour atteindre le niveau de fiabilité exigé. Parmi celles-ci on voit apparaître la vérification formelle du logiciel assistée par des outils (analyseurs statiques, prouveurs de programmes, etc). Cependant, la fiabilité de ces outils qui participent à la construction et la validation du logiciel est elle-même en question, menant à la conclusion que ces outils doivent eux-mêmes être formellement vérifiés. Je décrirai une avancée majeure dans cette direction : la preuve de correction, utilisant l’assistant de preuves Coq, du compilateur CompCert, un compilateur C réaliste et incluant un certain nombre d’optimisations.

Voir aussi


  • Aucun exposé du même auteur.
  • Recent Progress in Leakage-Resilient Cry...
    Yevgeniy Dodis
  • Composer le temps
    Gérard Berry
  • Approximation Bounds for Sparse Principa...
    Alexandre D’Aspremont
  • Diviser-pour-Régner & Inférence Statisti...
    Michael I. Jordan
  • Logarithmes discrets dans les corps fini...
    Antoine Joux
  • Une théorie de l'information mentale
    Claude Berrou
  • Exponential Mechanism for Social Welfar...
    Sampath Kannan
  • Untangling knots using combinatorial opt...
    Benjamin Burton
  • De la convexité tropicale aux jeux répé...
    Stéphane Gaubert
  • A Foundation for Flow-Based Program Matc...
    Julia Lawall
  • Construction à large couverture de la re...
    Benoît Crabbé
  • Définir et mesurer la complexité : la t...
    Jean-Paul Delahaye
  • Rendre la virgule flottante plus rigoure...
    Jean-Michel Muller
  • Approximations for stochastic graph rewr...
    Vincent Danos
  • Social Networks : a research vision and ...
    Peter Marbach
  • Three discrete geometric structures and ...
    Nabil Mustafa
  • From spanners to distance oracles and co...
    Laurent Viennot
  • Cognitive Computing
    Jérôme Pesenti
  • Vers les nouvelles bases de données pers...
    Serge Abiteboul
  • Structured Parallel Programming Primitiv...
    Vivek Sarkar
  • Manipuler les réseaux euclidiens
    Damien Sthelé
  • Réduction de modèles de voies de signali...
    Jérôme Feret
  • Le patient numérique personnalisé
    Nicholas Ayache
  • Scade 6: conception d'un langage de prog...
    Bruno Pagano
  • Co-Adaptive Instruments. Can we reinven...
    Wendy Mackay
  • Analyse de pire temps d’exécution et pro...
    Pascal Raymond
  • Chiffrer mieux pour (dé)chiffrer plus
    Anne Canteaut
  • New Results at the Crossroads of Convexi...
    Sébastien Bubeck
Auteur(s)
Xavier Leroy
INRIA
Informaticien

Plus sur cet auteur
Voir la fiche de l'auteur

Cursus :

Ancien élève de l'Ecole normale supérieure, Xavier Leroy est un informaticien français, directeur de recherche à l'INRIA. Il est connu pour être le principal concepteur et développeur du langage Objective Caml.

Il est un expert réputé dans le domaine des langages fonctionnels, de leur typage et de leur compilation. Ces dernières années, il a également beaucoup travaillé sur les méthodes formelles, les preuves formelles et la compilation certifiée. Il est notamment à la base du projet CompCert qui a réalisé un compilateur pour le Langage C entièrement certifié à l'aide de Coq.
Il est également l'auteur de LinuxThreads, qui était, avant la sortie de la version 2.6 du noyau Linux, la bibliothèque de threads la plus utilisée dans le système Linux.
En 2007, Xavier Leroy est lauréat du Prix Montpetit. En 2011, il est lauréat du prix La Recherche en sciences de l'information, en tant que représentant du projet CompCert. En 2012, il reçoit le prix "Microsoft Research Verified Software Milestone Award Citation", là encore en tant qu'architecte de CompCert.

Cliquer ICI pour fermer
Annexes
Téléchargements :
   - Télécharger la vidéo
   - Télécharger l'audio (mp3)

Dernière mise à jour : 22/04/2014