Show simple item record

dc.contributor.advisorMoore, J Strother, 1947-en
dc.creatorRay, Sandipen
dc.date.accessioned2008-08-28T22:41:23Zen
dc.date.available2008-08-28T22:41:23Zen
dc.date.issued2005en
dc.identifierb61122658en
dc.identifier.urihttp://hdl.handle.net/2152/2286en
dc.descriptiontexten
dc.description.abstractThe 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.
dc.format.mediumelectronicen
dc.language.isoengen
dc.rightsCopyright 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 the works.en
dc.subject.lcshAutomatic theorem provingen
dc.subject.lcshComputer programs--Verificationen
dc.subject.lcshComputer software--Verificationen
dc.subject.lcshIntegrated circuits--Verificationen
dc.subject.lcshAxiomsen
dc.titleUsing theorem proving and algorithmic decision procedures for large-scale system verificationen
dc.description.departmentComputer Sciencesen
dc.identifier.oclc70959957en
dc.type.genreThesisen
thesis.degree.departmentComputer Sciencesen
thesis.degree.disciplineComputer Sciencesen
thesis.degree.grantorThe University of Texas at Austinen
thesis.degree.levelDoctoralen
thesis.degree.nameDoctor of Philosophyen


Files in this item

Icon

This item appears in the following Collection(s)

Show simple item record