A robust machine code proof framework for highly secure applications

David S. Hardin, Eric W. Smith, William D. Young
[doi] [ISBN] [Google Scholar] [DBLP] [Citeseer]

Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and Its Applications
ACL2 '06
Seattle, Washington, USA
New York, NY, USA
Pages 11-20
Note(s): ISA specification, ACL2 theorem prover