Résumé
La satisfaction modulo théories (SMT) s’intéresse aux formules mathématiques mêlant la logique propositionnelle et des théories mathématiques décidables (ou quelquefois semi-décidables) : fonctions non-interprétées, théories arithmétiques diverses (programmation linéaire réelle ou entière, inéquations aux différences, arithmétique de Presburger avec addition et comparaisons, etc.), théorie des tableaux, manipulation de bitvecteurs, théories de pointeurs pour la gestion mémoire, etc. Comme les solveurs SMT, les solveurs SAT sont en progrès constant, en termes d’efficacité comme en termes d’applications. Ils sont de plus en plus utilisés en analyse statique et vérification de programmes, en programmation par contraintes, en optimisation, etc. Par exemple, comme l’a montré Thomas Jensen dans son séminaire du 4 novembre 2015 et comme le montrera Sylvain Conchon dans son séminaire ce jour, le couplage fort d’un langage de programmation bien conçu et d’un système SMT puissant permet une détection efficace de bugs dès l’écriture du programme, voire une preuve formelle complète de programmes dans certains cas.
Les formules traitées par les solveurs SMT font interagir très librement la logique et les différentes théories. Les solveurs les décomposent finement pour construire des formules propositionnelles telles que chaque atome appartient à une seule théorie, tout en permettant le partage de variables entre atomes. Nous montrons comment l’analyse de satisfiabilité des CNF obtenues par les solveurs SAT interagit avec les solveurs des théories particulières, et détaillons les difficultés de cette interaction. Nous présentons les théories principales utilisées en pratique, ainsi que les algorithmes sur lesquels elles se fondent. Nous montrons enfin comment des quantificateurs peuvent être introduits de façon à simplifier et généraliser les formules, en perdant la décidabilité d’une façon contrôlée au mieux. Le tout est illustré par des exemples liés à la vérification des programmes.
