A trustworthy monadic formalization of the ARMv7 instruction set architecture

DOI10.1007/978-3-642-14052-5_18zbMATH Open1291.68341OpenAlexW1863850585MaRDI QIDQ5747653FDOQ5747653

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

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

Mathematics Subject Classification ID

Cited In (10)

• Formal reasoning under cached address translation
• From Sets to Bits in Coq
• Automatic generation and validation of instruction encoders and decoders
• Safe functional systems through integrity types and verified assembly
• An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model
• Highly Automated Formal Proofs over Memory Usage of Assembly Code
• Improved Tool Support for Machine-Code Decompilation in HOL4
• Title not available (Why is that?)
• Lem: a lightweight tool for heavyweight semantics
• Parameterized synthesis for fragments of first-order logic over data words

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)