SAT-based String Solving : Solving String Constraints by Reduction to Boolean Satisfiability
String constraint solving is the task of checking whether first-order formulas over strings are satisfiable.Because strings are a core data type in nearly every programming language, reliable and efficient solvers are essential in many areas of formal verification. This thesis studies methods for solving string constraints by reducing them to propositional logic, allowing the satisfiability check to be delegated to a SAT solver. After an introduction to the underlying logical frameworks, it first explores propositional encodings for regular constraints. Although the presented method is not expressive enough to handle meaningful problems, it motivates the following chapter, which develops a general procedure for solving quantifier-free formulas over different types of string constraints. Beyond the propositional encodings, the chapter also investigates how to select an adequate alphabet and how to effectively conclude unsatisfiability. Finally, the thesis concludes with a more formal treatment of string constraint solving by presenting a formalization of the theory in Isabelle, an interactive theorem prover.
Preview
Rights
Use and reproduction:
Please note that individual components of the publication may be subject to other licensing or copyright conditions.
