%0 Journal Article
%T Abstract Stobjs and Their Application to ISA Modeling
%A Shilpi Goel
%A Warren A Hunt
%A Jr.
%A Matt Kaufmann
%J Electronic Proceedings in Theoretical Computer Science
%D 2013
%I Open Publishing Association
%R 10.4204/eptcs.114.5
%X 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.
%U http://arxiv.org/pdf/1304.7858v1