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 |