16 citations · 20 across the 4 of their papers we have counts for
5 papers
Verifying x86 Instruction Implementations
Shilpi Goel, Anna Slobodova, Rob Sumners +1
Verification of modern microprocessors is a complex task that requires a substantial allocation of resources. Despite significant progress in formal verification, the goal of compl…
Proceedings of the 15th International Workshop on the ACL2 Theorem Prover and Its Applications
Shilpi Goel, Matt Kaufmann
This volume contains the proceedings of the Fifteenth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2018), a two-day workshop held in Austin, Texas,…
Adding 32-bit Mode to the ACL2 Model of the x86 ISA
Alessandro Coglio, Shilpi Goel
The ACL2 model of the x86 Instruction Set Architecture was built for the 64-bit mode of operation of the processor. This paper reports on our work to extend the model with support…
The x86isa Books: Features, Usage, and Future Plans
Shilpi Goel
The x86isa library, incorporated in the ACL2 community books project, provides a formal model of the x86 instruction-set architecture and supports reasoning about x86 machine-code…
Abstract Stobjs and Their Application to ISA Modeling
Shilpi Goel, Warren A Hunt, Matt Kaufmann
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 tra…