Formally verified big step semantics out of x86-64 binaries

Ian Roessle, Freek Verbeek, Binoy Ravindran
[doi] [ISBN] [Google Scholar] [DBLP] [Citeseer]

Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs
CPP 2019
Cascais, Portugal
ACM
New York, NY, USA
Pages 181-195
2019
Note(s): x86 architecture, ISA specification