Après la présentation générale de la vérification formelle des programmes et circuits dans le cours 2014-2015, le cours 2015-2016 a été consacré aux méthodes automatiques de vérification fondées sur des théories décidables. Ces méthodes, introduites pour certaines dès les années 1960, ont fait des progrès considérables ces dernières années avec l’invention de nouveaux algorithmes remarquablement efficaces et la combinaison de ces algorithmes. Elles ont l’avantage de ne demander que peu de connaissances de leur fonctionnement interne à l’utilisateur, qui peut ainsi se consacrer davantage à sa propre problématique. Elles sont très utilisées industriellement dans le monde des circuits électroniques, soit pour vérifier le comportement, soit pour valider les nombreuses étapes de traitement de la spécification au masque de circuit final. En logiciel, elles sont de plus en plus utilisées comme complément idéal des systèmes de types pour détecter les erreurs dès la compilation, pour la recherche de bugs par analyse statique, et pour la génération automatique de tests dirigés.
Le cours a étudié les principales méthodes automatiques et leurs applications :
- d’abord, les binary decision diagrams (BDD), première structure de calcul booléen efficace déjà brièvement présentée et utilisée dans les cours précédents ;
- puis, les algorithmes analysant la satisfiabilité de grandes formules booléennes, ce qu’on appelle le problème SAT. Ils ont fait des progrès énormes ces vingt dernières années et sont devenus des outils standards dans de nombreux domaines de l’informatique, et les algorithmes SMT (satisfiabilité modulo théories), qui permettent de vérifier des formules arithmétiques ou symboliques bien plus riches ;
- ensuite, les algorithmes de vérification d’automates temporisés, adaptés à la validation des systèmes temps-réels ;
- enfin, les algorithmes explicites, qui énumèrent les états et transitions d’un système au lieu de le traiter symboliquement.