| An essential component in many verification methods is a fast decision procedure for validating logical expressions. This thesis presents several advances in the theory and implementation of such decision procedures, developed as part of ongoing efforts to improve the Stanford Validity Checker. We begin with the general problem of combining satisfiability procedures for individual theories into a satisfiability procedure for the combined theory. Two known approaches, those of Shostak and Nelson and Oppen, are described. We show how to combine these two methods to obtain the generality of the Nelson-Oppen method while retaining the efficiency of the Shostak method. We then present a general framework for combining decision procedures which includes features for enhancing performance and flexibility. Finally, validity checking requires that a heuristic search be built on top of the core decision procedure for satisfiability. We discuss strategies for efficient heuristic search and show how to adapt several powerful techniques from current research on Boolean satisfiability. Since these algorithms can be extremely subtle, a detailed proof of correctness is provided in the appendix. |
