Sciweavers

ITP
2010

A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture

13 years 7 months ago
A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture
Abstract. This paper presents a new HOL4 formalization of the current ARM instruction set architecture, ARMv7. This is a modern RISC architecture with many advanced features. The formalization is detailed and extensive. Considerable tool support has been developed, with the goal of making the model accessible and easy to work with. The model and supporting tools are publicly available – we wish to encourage others to make use of this resource. This paper explains our monadic specification approach and gives some details of the endeavours that have been made to ensure that the sizeable model is valid and trustworthy. A novel and efficient testing approach has been developed, based on automated forward proof and communication with ARM development boards.
Anthony C. J. Fox, Magnus O. Myreen
Added 15 Aug 2010
Updated 15 Aug 2010
Type Conference
Year 2010
Where ITP
Authors Anthony C. J. Fox, Magnus O. Myreen
Comments (0)