Design of decision procedures by combination and saturation
Conception de procédures de décision par combinaison et saturation
Résumé
Many applications of formal methods rely on generating formulae of first order logic and proving or disproving their satisfiability with respect to some background theory, which is often obtained as a combination of several theories. In the literature, this kind of satisfiability problem is called Satisfiability Modulo Theories (SMT). In this thesis, we focus on the design of decision procedures for SMT problems by integrating saturation techniques based on rewriting for finitely axiomatized theories, together with combination techniques for unions of theories. The first contribution of the thesis is a rational reconstruction of the combination methods proposed by Nelson-Oppen, Shostak and others in an uniform framework. This is the starting point for further investigations. We then introduce the concept of extended canonizer and derive a modularity result for a new class of theories. This is in contrast with the lack of modularity of the class of theories considered by the Shostak method. The second contribution concerns the problem of combining rewriting-based satisfiability procedures using the Nelson-Oppen method. We use meta-saturation to develop automatic proof techniques to check important requirements for the combinability of such procedures. When meta-saturation halts for a theory, its output allows us to reason about the combinability of a rewriting-based satisfiability procedure for this theory. The third contribution of this thesis is about the integration of decision procedures into SMT solvers. We consider the problem of augmenting decision procedures with the capability of computing conflict sets without degrading performances, as well as the problem of modularly constructing conflict sets for a combined theory. In this respect, we extend the Nelson-Oppen combination method to modularly build conflict sets for disjoint unions of theories. We also study how the computed conflict sets relate to an appropriate notion of minimality.
Beaucoup d'applications des méthodes formelles reposent sur la génération de formules en logique du premier ordre et la preuve de leur satisfiabilité par rapport à une théorie en arrière-plan, qui est souvent obtenu par mélange de plusieurs théories. Dans la littérature, cette forme de satisfiabilité est appelée Satisfiabilité Modulo Théories (SMT). Dans cette thèse, on s'intéresse à la conception de procédures de décision pour les problèmes SMT, en intégrant des techniques de saturation basées sur la réécriture pour des theories finiment axiomatisées et des techniques de combinaison pour des unions de théories. La première contribution de cette thèse est une reconstruction raisonnée, dans un cadre uniforme, des méthodes de combinaison proposées par Nelson-Oppen, Shostak et d'autres. Ceci est le point de départ pour de nouvelles investigations. Nous introduisons ensuite le concept de canoniseur étendu et dérivons un résultat de modularité pour une nouvelle classe de théories, ce qui contraste avec l'absence de modularité pour la classe de théories considérée par Shostak. La deuxième contribution concerne le problème de la combinaison de procédures basées sur la réécriture en utilisant la méthode de Nelson-Oppen. Nous utilisons la méta-saturation pour développer des techniques de preuve automatique permettant de tester les conditions pour la combinabilité de telles procédures. Lorsque la méta-saturation termine pour une théorie, le résultat obtenu permet de raisonner sur la combinabilité pour cette théorie d'une procédure de satisfiabilité basée sur la réécriture. La troisième contribution de cette thèse est liée à l'intégration des procédures de décision dans les solveurs SMT. Nous considérons le problème de rajouter aux procédures de décision la capacité de construire des justifications en cas d'insatisfiabilité, sans dégradation des performances, en nous focalisant sur la construction modulaire de telles justifications pour une théorie combinée. Pour ce faire, nous étendons la méthode de combinaison de Nelson-Oppen de manière à construire de faÐcon modulaire des justifications d'insatisfiabilité pour des unions de théories. Nous étudions également comment les justifications obtenues peuvent être reliées à une forme appropriée de minimalité.