Generalization, lemma generation, and induction in ACL2

Simple item page
dc.contributor.advisorMoore, J. Strother, 1947-en
dc.creatorErickson, John D., Ph. D.en
dc.date.accessioned2008-08-29T00:25:17Zen
dc.date.accessioned2017-05-11T22:19:33Z
dc.date.available2008-08-29T00:25:17Zen
dc.date.available2017-05-11T22:19:33Z
dc.date.issued2008-05en
dc.descriptiontexten
dc.description.abstractFormal verification is becoming a critical tool for designing software and hardware today. Rising complexity, along with software's pervasiveness in the global economy have meant that errors are becoming more difficult to find and more costly to fix. Among the formal verification tools available today, theorem provers offer the ability to do the most complete verification of the most complex systems. However, theorem proving requires expert guidance and typically is too costly to be economical for all but the most mission critical systems. Three major challenges to using a theorem prover are: finding generalizations, choosing the right induction scheme, and generating lemmas. In this dissertation we study all three of these in the context of the ACL2 theorem prover.en
dc.description.departmentComputer Sciencesen
dc.format.mediumelectronicen
dc.identifierb70710314en
dc.identifier.oclc244394857en
dc.identifier.urihttp://hdl.handle.net/2152/4004en
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.lcshFormal methods (Computer science)en
dc.subject.lcshComputer programs--Verificationen
dc.subject.lcshAutomatic theorem provingen
dc.titleGeneralization, lemma generation, and induction in ACL2en
dc.type.genreThesisen

Files

Collections

University of Texas at Austin