A verified framework for symbolic execution in the ACL2 theorem prover
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 practic...
| Main Author: | |
|---|---|
| Format: | Others |
| Language: | English |
| Published: |
2011
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/2152/ETD-UT-2010-12-2210 |