Mechanized theorem proving is a promising means of formally
establishing facts about complex systems. However, in applying
theorem proving methodologies to industrial-scale hardware and
software systems, a large amount of user interaction is required in
order to prove useful properties. In practice, the human user tasked
with such a verification must gain a deep understanding of the system
to be verified, and prove numerous lemmas in order to allow the
theorem proving program to approach a proof of the desired fact.
Furthermore, proofs that fail during this process are a source of
confusion: the proof may either fail because the conjecture was false,
or because the prover required more help from the user in order to
reach the desired conclusion.
We have implemented a symbolic execution framework inside the ACL2
theorem prover in order to help address these issues on certain
problem domains. Our framework introduces a proof strategy that
applies bit-level symbolic execution using BDDs to finite-domain
problems. This proof strategy is a fully verified decision procedure
for such problems, and on many useful problem domains its capacity
vastly exceeds that of exhaustive testing. Our framework also
produces counterexamples for conjectures that it determines to be
false.
Our framework seeks to reduce the amount of necessary user interaction
in proving theorems about industrial-scale hardware and software
systems. By increasing the automation available in the prover, we
allow the user to complete useful proofs while understanding less of
the detailed implementation of the system. Furthermore, by producing
counterexamples for falsified conjectures, our framework reduces the
time spent by the user in trying to determine why a proof failed. / text
| Identifer | oai:union.ndltd.org:UTEXAS/oai:repositories.lib.utexas.edu:2152/ETD-UT-2010-12-2210 |
| Date | 11 February 2011 |
| Creators | Swords, Sol Otis |
| Source Sets | University of Texas |
| Language | English |
| Detected Language | English |
| Type | thesis |
| Format | application/pdf |
Page generated in 0.0024 seconds