|dc.contributor.advisor||Moore, J Strother, 1947-||en
|dc.description.abstract||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.
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.||
|dc.rights||Copyright is held by the author. Presentation of this material on
the Libraries' web site by University Libraries, The University of Texas at Austin was made
possible under a limited license grant from the author who has retained all copyrights in
|dc.subject.lcsh||Automatic theorem proving||en
|dc.title||Using theorem proving and algorithmic decision procedures for large-scale system verification||en
|thesis.degree.grantor||The University of Texas at Austin||en
|thesis.degree.name||Doctor of Philosophy||en