For the third junior seminary (open to all), organised by the liris phd students, Gerard Berry (Golden medal from the CNRS, Member of the "Académie des Sciences", Professor at "College de France" with a chair on Algorithms, computers and languages) will present a talk about the bug hunt in computer sciences

Presented in French, the talk will be named "A la chasse aux bugs".

It will be held in the amphiteatre BERGER,  LyonTech-la Doua - 10 rue de la Physique, 69621 Villeurbanne (tramway stop: Gaston Berger) (http://plan.univ-lyon1.fr/plans/fiches_insa/berger.html)

Summary (in French):

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.