Improved Tool Support for Machine-Code Decompilation in HOL4

DOI10.1007/978-3-319-22102-1_12zbMath1465.68048OpenAlexW2166304444MaRDI QIDQ2945632

A. C. J. Fox

Publication date: 14 September 2015

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

Full work available at URL: https://doi.org/10.1007/978-3-319-22102-1_12

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (2)

Bidirectional grammars for machine-code decoding and encoding ⋮ An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model

Uses Software

• HOL
• CakeML
• GDSL
• Rocksalt
• TSL

Cites Work

• High-level separation logic for low-level code
• LCF-Style Bit-Blasting in HOL4
• Using XCAP to Certify Realistic Systems Code: Machine Context Management
• CakeML
• A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture
• Hoare Logic for Realistically Modelled Machine Code

This page was built for publication: Improved Tool Support for Machine-Code Decompilation in HOL4