Abstract Stobjs and Their Application to ISA Modeling

Shilpi Goel
(Department of Computer Science, University of Texas at Austin) 		Warren A Hunt, Jr.
(Department of Computer Science, University of Texas at Austin) 		Matt Kaufmann
(Department of Computer Science, University of Texas at Austin)

We introduce a new ACL2 feature, the abstract stobj, and show how to apply it to modeling the instruction set architecture of a microprocessor. Benefits of abstract stobjs over traditional ("concrete'') stobjs can include faster execution, support for symbolic simulation, more efficient reasoning, and resilience of proof developments under modeling optimization.

In Ruben Gamboa and Jared Davis: Proceedings International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2013), Laramie, Wyoming, USA , May 30-31, 2013, Electronic Proceedings in Theoretical Computer Science 114, pp. 54–69.
Published: 26th April 2013.
ArXived at: https://dx.doi.org/10.4204/EPTCS.114.5 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org