Decision Procedures for Program Synthesis and Verification

Decision procedures are widely used in software development and verification. The goal of this dissertation is to increase the scope of properties that can be verified using decision procedures. To achieve this goal, we identify three improvements over the state of the art in decision procedures, and their use in software reliability tools. First, we observe that developing new decision procedures increases the range of properties and programs that are amenable to automated verification. In this thesis, we are particularly interested in the verification of container data structures. Existing verification tools use set abstractions to reason about the contents of data structures. However, set abstraction loses any information about duplicate occurrences of elements in a container. We therefore propose a new logic for reasoning about multisets with cardinality constraints. This logic subsumes reasoning about sets and enables reasoning about duplicate elements in containers. Cardinality constraints are useful for reasoning about the number of elements stored in a data structure. Based on an extension of linear arithmetic (which we call LIA*), we describe a decision procedure for the logic ofmultisets with cardinalities. By investigating properties of LIA*, we prove that the satisfiability of multisets with cardinality constraints is an NP-complete problem. Second, we notice that verification conditions expressing properties of data structures often can be decomposed into several well-understood logics. If the signatures of the component theories are not disjoint (i.e., they sharemore than equality) then it is often unclear whether such a reduction is possible, even if individual decision procedures for all component theories are known to exist. We investigate how to combine non-disjoint theories that share set symbols and operators. We state and prove a new combination theorem for such theories. Our theorem states that the combination is possible if each component theory can be reduced to the common theory, the theory of sets with cardinality constraints. We prove that many theories satisfy this property. The resulting combined logic enables reasoning about complex properties of data structure implementations that could not be expressed in any previously known decidable logic. Finally, we identify new applications of decision procedures in software reliability tools. We describe how a model-producing decision procedure can be generalized into a predictable and complete synthesis procedure. Given a specification, a synthesis procedure is an algorithm that outputs the code that meets this specification. We demonstrate this approach in detail for the concrete case of linear integer arithmetic. We further develop an orthogonal approach to use decision procedure for program synthesis: we show how to reconstruct code snippets that satisfy given type constraints from a proof of unsatisfiability that was computed by a theorem prover. The programmer then interactively selects the desired code snippet from a choice of code snippets generated by the synthesis engine. Together, our results provide the foundations of sound and predictable verification and synthesis tools for integer arithmetic and container data structures.