Abstract Stobjs and Their Application to ISA Modeling
Shilpi Goel, Warren A. Hunt, Matt Kaufmann · Electronic Proceedings in Theoretical Computer Science · 2013
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.