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...

Full description

Bibliographic Details
Main Author: Swords, Sol Otis
Format: Others
Language:English
Published: 2011
Subjects:
Online Access:http://hdl.handle.net/2152/ETD-UT-2010-12-2210