Improved tool support for machine-code decompilation in HOL4

Anthony C. J. Fox
[doi] [Google Scholar] [DBLP] [Citeseer]

Proceedings 6th International Conference Interactive Theorem Proving ITP 2015
LNCS, volume 9236
Nanjing, China
Springer
Pages 187-202
August 2015
Note(s): Arm architecture, ISA specification, instruction set architecture