Le cours de cette année inaugure un cycle pluriannuel dédié au développement formel des programmes et circuits. Son objet principal sera l’étude des méthodes et outils de vérification formelle, qui cherchent à établir des preuves mathématiques de correction totale (la réalisation implémente toute la spécification et rien qu’elle) ou partielle (certains types de bugs ne peuvent pas se produire). Les techniques associées sont fondées sur des approches mathématiques et algorithmiques variées. Elles sont implémentées dans des systèmes de vérification allant du prototype de recherche à l’outil industriel effectivement utilisé de façon routinière dans des domaines industriels spécifiques.
Le développement de logiciel ou de circuits s’appuie traditionnellement sur un modèle de travail descendant de la conception à l’implémentation, puis remontant du test unitaire des composants logiciels vers le test d’intégration. La validation de l’application est ainsi exclusivement fondée sur des jeux de tests, souvent développés de façon artisanale en fonction de spécifications informelles. Cette méthode est raisonnablement efficace pour les programmes prenant des données assez uniformes au début de leur exécution et rendant des résultats à la fin de cette exécution. Mais elle s’avère souvent insuffisante pour des programmes pour lesquels les bugs peuvent avoir des conséquences directes ou indirectes redoutables : ceux dont les entrées sont très variées, comme les compilateurs qui doivent rejeter ou traduire correctement tous les programmes possibles, les programmes qui agissent en permanente interaction avec leur environnement comme les systèmes d’exploitation et les applications distribuées sur le Web, les programmes réactifs qui servent à contrôler les systèmes cyber-physiques qui interagissent en temps réel avec un environnement physique complexe (transports, robots, etc.), les protocoles subtils qui assurent la sécurité informatique, les systèmes de vote électronique, etc. Les conditions d’exécution peuvent alors être extrêmement nombreuses et intestables en totalité. De plus, si le test permet la validation des comportements ou la détection de bugs pour les conditions d’exécution effectivement examinées, il ne dit absolument rien sur les autres.