An increasing number of applications in verification and security rely on or could benefit from automatic solvers that can check the satisfiability of constraints over a rich set of data types that includes character strings. Unfortunately, most string solvers today are standalone tools that can reason only about some fragment of the theory of strings and regular expressions, sometimes with strong restrictions on the expressiveness of their input language (such as, length bounds on all string variables). These specialized solvers reduce string problems to satisfiability problems over specific data types, such as bit vectors, or to automata decision problems. On the other side, despite their power and success as back-end reasoning engines, general-purpose Satisfiability Modulo Theories (SMT) solvers so far have provided minimal or no native support for string reasoning. This thesis presents a deductive calculus describing a new algebraic approach that allows solving constraints over the theory of unbounded strings and regular expressions natively, without reduction to other problems. We provide proofs of refutation soundness and solution soundness of our calculus, and solution completeness under a fair proof strategy. Moreover, we show that our calculus is a decision procedure for the theory of regular language membership with length constraints. We have implemented our calculus as a string solver for the theory of (unbounded) strings with concatenation, length, and membership in regular languages, and incorporated it into the SMT solver CVC4 to expand its already large set of built-in theories. This work makes CVC4 the first SMT solver that is able to accept and process a rich set of mixed constraints over strings, integers, reals, arrays and other data types. In addition, our initial experimental results show that, over string problems, CVC4 is highly competitive with specialized string solvers with a comparable input language. We believe that the approach we described in this thesis provides a new idea for string-based formal methods.

Le raisonnement assisté par ordinateur joue un rôle crucial en informatique et en logique mathématique, de la programmation logique à la déduction automatique, en passant par les assistants à la démonstration. Le but de cette thèse est la conception d'un cadre général où différentes techniques de raisonnement assisté par ordinateur peuvent être implémentées, pour que ces dernières puissent collaborer, être généralisées, et être implémentées de manière plus sûre. Le cadre que je propose est un calcul des séquents appelé LKp(T), qui généralise un système de la littérature à la présence d'une théorie pour laquelle nous avons une procédure de décision, comme l'arithmétique linéaire. Cette thèse développe la méta-théorie de LKp(T), avec par exemple la propriété de complétude logique. Nous montrons ensuite comment le système spécifie une procédure de recherche de preuve qui émule une technique connue du domaine de la Satisfiabilité-modulo-théories appelée DPLL(T). Enfin, les tableaux de clauses et les tableaux de connexions sont d'autres techniques populaires en déduction automatique, d'une nature relativement différente de DPLL. Cette thèse décrit donc également comment ces techniques de tableaux peuvent être décrites en termes de recherche de preuve dans LKp(T). La simulation est donnée à la fois pour la logique propositionnelle et la logique du premier ordre, ce qui ouvre de nouvelles perspectives de généralisation et de collaboration entre les techniques de tableaux et DPLL, même en présence d'une théorie.