Le troisième séminaire junior (ouvert à tous), organisé par les doctorants du LIRIS, aura lieu le mardi 7 juin 2016 à 10h00 et sera animé par Gérard Berry (Médaille d'or du CNRS, Membre de l'Académie des sciences, Professeur au Collège de France où il est titulaire de la chaire "Algorithme, machines et langages" ).

Il présentera à cette occasion un exposé intitulé : A la chasse aux bugs.

Le séminaire aura lieu Amphy BERGER, LyonTech-la Doua - 10 rue de la Physique, 69621 Villeurbanne (arrêt tramway : Université Lyon 1) (http://plan.univ-lyon1.fr/plans/fiches_insa/berger.html)

Résumé :

L’informatique est un combat permanent entre deux exacts opposés: nous-mêmes les spécifieurs et programmeurs, imaginatifs mais lents et peu rigoureux, et les microprocesseurs, stupides mais hyper-rapides et totalement rigoureux. Le trajet de l’idée au programme qui marche est donc intrinsèquement difficile, et il doit être parfaitement  maîtrisé pour éviter les bugs sournois qui résultent toujours d’une défaillance de l’homme et pas de la machine. Pour mieux comprendre leur nature profonde, nous analyserons certains bugs célèbres ou moins connus, dans lesquels l’ordinateur a amplifié des micro-erreurs en désastres ou encore provoqué des failles de sécurité facilement exploitables. Nous analyserons ensuite les méthodes qui permettent de chasser efficacement les bugs, le test classique s’avérant par nature insuffisant : s'il permet de trouver des erreurs, il est inopérant pour montrer leur absence. Nous verrons que le test aléatoire bien dirigé peut donner des résultats étonnants, par exemple en exhibant des centaines d’erreurs dans les compilateurs C actuellement disponibles. Nous présenterons ensuite les méthodes formelles qui permettent de démontrer automatiquement l’absence de certaines erreurs dans les circuits et programmes, voir même de prouver la correction totale du comportement comme pour l’arithmétique du Pentium chez Intel ou le compilateur C CompCert développé par Xavier Leroy et son équipe à l’Inria.