A trustworthy monadic formalization of the ARMv7 instruction set architecture

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

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

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
• Lem: A Lightweight Tool for Heavyweight Semantics
• 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?)
• Parameterized synthesis for fragments of first-order logic over data words

Uses Software

• CoqJVM
• HOL

   Recommendations

• Formalizing SPARCv8 Instruction Set Architecture in Coq 👍 👎
• Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties 👍 👎
• Title not available (Why is that?) 👍 👎
• Hoare Logic for ARM Machine Code 👍 👎
• Title not available (Why is that?) 👍 👎

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)