Using theorem proving and algorithmic decision procedures for large-scale system verification

The goal of formal verification is to use mathematical methods to prove that a computing system meets its specifications. When applicable, it provides a higher assurance than simulation and testing in correct system execution. However, the capacity of the state of the art in formal verification today is still far behind what is necessary for its widespread adoption in practice. In this dissertation, we devise methods to increase the capacity of formal verification. Formal verification techniques can be broadly divided into two categories, namely deductive techniques or theorem proving, and decision procedures such as model checking, equivalence checking, and symbolic trajectory evaluation. Neither deductive nor algorithmic techniques individually scale up to the size of modern industrial systems, albeit for orthogonal reasons. Decision procedures suffer from state explosion. Theorem proving requires manual assistance. Our methods involve a sound, efficient, and scalable integration of deductive and algorithmic techniques. ix There are four main contributions in this dissertation. First, we present several results that connect different deductive proof styles used in the verification of sequential programs. The connection allows us to efficiently combine theorem proving with symbolic simulation to prove the correctness of sequential programs without requiring a verification condition generator or manual construction of a global invariant. Second, we formalize a notion of correctness for reactive concurrent programs that affords effective reasoning about infinite computations. We discuss several reduction techniques that reduce the correctness proofs of concurrent programs to the proof of an invariant. Third, we present a method to substantially automate the process of discovering and proving invariants of reactive systems. The method combines term rewriting with reachability analysis to generate efficient predicate abstractions. Fourth, we present an approach to integrate model checking procedures with deductive reasoning in a sound and efficient manner. We use the ACL2 theorem prover to demonstrate our methods. A consequence of our work is the identification of certain limitations in the logic and implementation of ACL2. We recommend several augmentations of ACL2 to facilitate deductive verification of large systems and integration with decision procedures.