{Conférence} - "A la chasse aux bugs"

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. Gérard Berry est Médaille d’or du CNRS 2015. Sa contribution scientifique concerne cinq sujets : - le lambda calcul et la programmation fonctionnelle ; - la programmation parallèle et temps réel ; - la conception assistée par ordinateur de circuits intégrés synchrones ; - la vérification formelle de programmes et circuits ; - la modélisation du calcul en général. Il est le créateur principal du langage de programmation Esterel et de son outillage.