ARM in HOL

The development repository is located at SourceForge.

Validation test results are located here.

A web-based tool for evaluating the model is located here.

Bibliography

Anthony Fox and Magnus O. Myreen. A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture. In Interactive Theorem Proving (ITP), 2010.

Anthony C. J. Fox, Michael J. C. Gordon, and Magnus O Myreen. Specification and verification of ARM hardware and software. In David S. Hardin, editor, Design and Verification of Microprocessor Systems for High-Assurance Applicaions, pages 221-248. Springer, 2010.

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 O. Myreen, Anthony C. J. Fox and Michael J. C. Gordon. Hoare Logic for ARM Machine Code. In Fundamentals of Software Engineering (FSEN), 2007.

Hompages

Anthony Fox, Magnus Myreen and Mike Gordon.