Showing cs.LOShow all
2 papers · 1 filter
cs.LO2019
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…
cs.LO2018
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…