Résumé
Le cours commencera par la présentation générale des cours de l’année 2016, consacrés aux structures de données et algorithmes pour la vérification formelle. Le cadre de ces cours sera limité à la vérification automatique, principalement dans les cas décidables.
Après une présentation générale des cours de l’année 2016 suivie d’un rappel des notions principales de complexité algorithmique et de calcul booléen, le cours a étudié les diagrammes de décisions binaires ou BDD (binary decision diagrams). Ce sont les premières structures à avoir révolutionné le calcul booléen, essentiel dans de nombreux domaines applicatifs, mais qu’on a longtemps pensé inutilisable en pratique de par sa complexité : la satisfaction booléenne est le prototype du problème NP-complet.
Les BDDs ont été introduits par plusieurs auteurs dans les années 1970, mais surtout systématisés et mis en pratique grâce au travail fondamental de Randy Bryant à Carnegie-Mellon à la fin des années 1980. Ce sont des graphes avec partage maximal réalisant une forme canonique compacte des expressions Booléennes, modulo la donnée d’un ordre des variables apparaissant dans ces expressions. La canonicité implique que l’égalité de fonctions Booléennes se décide en temps constant, les opérations logiques se faisant elles en temps polynomial d’une façon récursive simple. Nous étudierons l’implémentation efficace des BDDs, puis montrerons l’influence décisive de l’ordre des variables sur leur taille, ainsi que les heuristiques permettant d’éviter autant que possible leur explosion en mémoire. À travers des exemples liés au langage Esterel étudié les années précédentes, nous expliquerons pourquoi les BDDs sont bien adaptés à la synthèse, l’optimisation et la vérification de circuits ou de contrôle complexe dans les programmes logiciels. Le séminaire qui suivra approfondira ces questions dans le domaine des circuits électroniques.
