A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture
作者： Anthony Fox , Magnus O. Myreen
DOI: 10.1007/978-3-642-14052-5_18
关键词: Development (topology) 、 Architecture 、 Programming language 、 ARM architecture 、 Instruction set 、 Machine code 、 Reduced instruction set computing 、 Computer science 、 Resource (project management) 、 Proof assistant
摘要: This paper presents a new HOL4 formalization of the current ARM instruction set architecture, ARMv7. is modern RISC architecture with many advanced features. The detailed and extensive. Considerable tool support has been developed, goal making model accessible easy to work with. supporting tools are publicly available – we wish encourage others make use this resource. explains our monadic specification approach gives some details endeavours that have made ensure sizeable valid trustworthy. A novel efficient testing based on automated forward proof communication development boards.
springer.com
core.ac.uk
springerlink.com
chalmers.se 参考文章(20)
Roch Guerin, Ramesh Govindan, Greg Minshall, Proceedings of the 2005 conference on Applications, technologies, architectures, and protocols for computer communications acm special interest group on data communication. ,(2005)
Jason J. Gosior, Phillip Jacobsen, Colin C. Broughton, John F. Sobota, System on chip architecture ,(2002)
Magnus O. Myreen, Michael J. C. Gordon, Verified LISP Implementations on ARM, x86 and PowerPC theorem proving in higher order logics. pp. 359- 374 ,(2009) , 10.1007/978-3-642-03359-9_25
Warren A. Hunt, Sol Swords, Centaur Technology Media Unit Verification computer aided verification. pp. 353- 367 ,(2009) , 10.1007/978-3-642-02658-4_28
Maribel Fernández, Murdoch J. Gabbay, Curry-style types for nominal terms types for proofs and programs. pp. 125- 139 ,(2006) , 10.1007/978-3-540-74464-1_9
Anthony Fox, Formal Specification and Verification of ARM6 theorem proving in higher order logics. pp. 25- 40 ,(2003) , 10.1007/10930755_2
Robert Atkey, CoqJVM: an executable specification of the Java virtual machine using dependent types types for proofs and programs. pp. 18- 32 ,(2007) , 10.1007/978-3-540-68103-8_2
John L. Hennessy, David A. Patterson, Computer Architecture: A Quantitative Approach ,(1989)
Steve Furber, ARM System-on-Chip Architecture ,(2000)
David Aspinall, Jaroslav Ševčík, Formalising java's data race free guarantee theorem proving in higher order logics. pp. 22- 37 ,(2007) , 10.1007/978-3-540-74591-4_4