A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture
From MaRDI portal
Publication:5747653
DOI10.1007/978-3-642-14052-5_18zbMath1291.68341OpenAlexW1863850585MaRDI QIDQ5747653
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
Related Items (9)
Automatic generation and validation of instruction encoders and decoders ⋮ Improved Tool Support for Machine-Code Decompilation in HOL4 ⋮ Parameterized synthesis for fragments of first-order logic over data words ⋮ Formal reasoning under cached address translation ⋮ Safe functional systems through integrity types and verified assembly ⋮ Highly Automated Formal Proofs over Memory Usage of Assembly Code ⋮ An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model ⋮ From Sets to Bits in Coq ⋮ Lem: A Lightweight Tool for Heavyweight Semantics
Uses Software
This page was built for publication: A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture
