A trustworthy monadic formalization of the ARMv7 instruction set architecture

Anthony C. J. Fox, Magnus O. Myreen
[doi] [Google Scholar] [DBLP] [Citeseer]

Proceedings Interactive Theorem Proving ITP 2010
LNCS, volume 6172
Springer
Pages 243-258
2010
Note(s): Arm architecture, ISA specification, instruction set architecture