Prouver les programmes : pourquoi, quand, comment

[Gérard Berry]

Tel est le titre général du cours 2014-2015 et de ceux des années qui vont suivre. La méthode classique de mise au point des programmes informatiques est le test, réalisé soit à partir de fichiers décrivant des données et événements en entrée de l’application, soit en situation physique pour les circuits et les logiciels embarqués. Le test permet effectivement de trouver des bugs, mais son insuffisance fondamentale est qu’il ne permet jamais d’en assurer l’absence. Ceci a été reconnu très tôt, dès 1949 dans un papier visionnaire d’Alan Turing qui a suggéré de remplacer les tests par de véritables preuves mathématiques de correction des programmes. De nombreux chercheurs ont travaillé sur le sujet depuis les débuts de l’informatique, initialement de façon surtout académique. Ils ont développé plusieurs types de méthodes de vérification formelle des programmes et circuits : par assertions, par réécriture, par interprétation abstraite, par déduction logique, par vérification de modèles, etc. Ce travail fondamental mais difficile et de long terme a aussi permis de bien mieux comprendre la conception et la sémantique formelle des langages de programmation et des programmes eux-mêmes, et aussi de faire des progrès considérables dans le domaine plus mathématique de la logique formelle.

L’arrivée à maturité de plusieurs systèmes informatiques de vérification automatique ou d’assistants de preuve a permis de faire passer la vérification formelle à l’échelle des vraies applications, y compris industrielles : vérifications de propriétés clefs de sécurité en avionique (Dassault Aviation avec Esterel), vérification de la conduite de RER et métros (avec la Méthode B de Jean-Raymond Abrial), correction de l’arithmétique flottante du Pentium (par John Harrison avec HOL-Light pour Intel et David Rusinoff et. al. avec ACL2 pour AMD), vérification systématique des étapes de synthèses de circuits électroniques (techniques efficaces de model-checking à base de calculs formels BDD, SAT et SMT), vérification de systèmes d’aiguillage et de routage de trains dans de grandes gares (par Prover Technologies) vérification du noyau de système d’exploitation SeL4 (par Gerwin Klein et. al. avec l’assistant de preuve Isabelle), vérification du compilateur C CompCert (par Xavier Leroy avec Coq). De façon plus surprenante, les techniques originellement développées pour l’informatique ont aussi trouvé des applications en mathématiques, avec les preuves par Georges Gonthier de théorèmes de grande ampleur comme le théorème des 4 couleurs et surtout le théorème de Feit-Thompson sur la classification des groupes finis d’ordre impair. (À noter que Gorges Gonthier avait fait auparavant des contributions fondamentales sur Esterel dans sa thèse). De façon intéressante, ces preuves mathématiques sur ordinateur nous apprennent beaucoup sur les architectures techniques nécessaires pour la preuve de gros programmes.

L’ambition du cours 2014-2015 sera de présenter le problème et les différentes méthodes de preuve ou dans un cadre général, présentation non disponible à l’heure actuelle car les méthodes précitées ont été développées en ordre plutôt dispersé. Les cours des années suivantes rentreront davantage dans le détail des principales méthodes et de leurs applications.