L'implantation et la preuve de correction d'algorithmes pour combiner des procédures de décision est un défi important dans le domaine de la vérification. Dans cet exposé, je présenterai une machine abstraite pour combiner des procédures de décision basée sur la procédure classique de Nelson-Oppen et incluant de nombreuses optimisations: abstraction de variable avec partage, normalisation des termes, et génération à la Shostak de nouvelles égalités pour les théories avec solvers.
La sémantique de cette machine est présentée à l'aide d'un système de règles d'inférence dont la précision est suffisamment fine pour modéliser la plupart des mécanismes utilisés aujourd'hui pour combiner des procédures de décision. En particulier, à l'aide d'un simple langage d'expressions régulières, nous pouvons décrire plusieurs algorithmes de combinaison comme des statégies particulières de nos régles d'inférence, depuis la méthode de base de Nelson-Oppen jusqu'à l'algorithme très optimisé présenté récemment par Sankar et Ruess.
La version de base de cette machine est présentée à l'aide d'un système d'inférence non-déterministe et très généraliste, ce qui permet d'obtenir des preuves de correction très simples pouvant être étendues de manière modulaire à chaque fois qu'une nouvelle caractéristique est ajoutée au système. De la même manière, la preuve de correction d'une nouvelle stratégie ne demande qu'un effort minimal.