Formal 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. / text
| Identifer | oai:union.ndltd.org:UTEXAS/oai:repositories.lib.utexas.edu:2152/4004 |
| Date | 29 August 2008 |
| Creators | Erickson, John D., Ph. D. |
| Source Sets | University of Texas |
| Language | English |
| Detected Language | English |
| Type | Thesis |
| Format | electronic |
| 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 the works. |
Page generated in 0.0025 seconds