Simulation and formal verification of x86 machine-code programs that make system calls

Shilpi Goel, Warren A. Hunt Jr., Matt Kaufmann, Soumava Ghosh
[doi] [Google Scholar] [DBLP] [Citeseer]

Formal Methods in Computer-Aided Design, FMCAD
Pages 91-98
2014
Note(s): ISA specification, x86 architecture, instruction set architecture, ACL2 theorem prover