A trustworthy monadic formalization of the ARMv7 instruction set architecture

DOI10.1007/978-3-642-14052-5_18MaRDI QIDQ5747653zbMATH OpenOpenAlexFDO

Authors A. C. J. Fox, Magnus O. Myreen

Publication date 14 September 2010

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-14052-5_18

Mathematics Subject Classification ID

Recommendations

• Formalizing SPARCv8 instruction set architecture in Coq
• Machine assisted proof of ARMv7 instruction level isolation properties
• scientific article; zbMATH DE number 1670745
• Hoare Logic for ARM Machine Code
• scientific article; zbMATH DE number 1670746

Cited in

(13)

• Formalizing SPARCv8 instruction set architecture in Coq
• Parameterized synthesis for fragments of first-order logic over data words
• Automatic generation and validation of instruction encoders and decoders
• Formal reasoning under cached address translation
• Lem: a lightweight tool for heavyweight semantics
• An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model
• scientific article; zbMATH DE number 1670745 (Why is no real title available?)
• Highly automated formal proofs over memory usage of assembly code
• Safe functional systems through integrity types and verified assembly
• Physical addressing on real hardware in Isabelle/HOL
• From Sets to Bits in Coq
• Machine assisted proof of ARMv7 instruction level isolation properties
• Improved tool support for machine-code decompilation in HOL4

Describes a project that uses

Uses Software

• CoqJVM
• HOL

This page was built for publication: A trustworthy monadic formalization of the ARMv7 instruction set architecture

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5747653)