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. |
ArXived at: https://dx.doi.org/10.4204/EPTCS.114.5 | bibtex | |
Comments and questions to: eptcs@eptcs.org |
For website issues: webmaster@eptcs.org |