ARM in HOL
The development repository is located at GitHub.
Validation test results are located here.
A web-based tool for evaluating the model is located here.
Jade Alglave, Anthony Fox, Samin Ishtiaq, Magnus O. Myreen, Susmit Sarkar, Peter Sewell, and Francesco Zappa Nardelli. The Semantics of Power and ARM Multiprocessor Machine Code. DAMP 09.
, Magnus Myreen
and Mike Gordon