Machine instruction syntax and semantics in higher order logic

DOI10.1007/10721959_2MaRDI QIDQ2723406zbMATH OpenFDO

Authors Neophytos Michael, Andrew W. Appel

Publication date 5 July 2001

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/10721959_2

Mathematics Subject Classification ID

Recommendations

• A semantic model of types and machine instructions for proof-carrying code
• Hoare Logic for ARM Machine Code
• A tutorial example of the semantic approach to foundational proof-carrying code
• Tutorial examples of the semantic approach to foundational proof-carrying code
• A tutorial example of the semantic approach to foundational proof-carrying code: Abstract

Cited in

(9)

• Safe functional systems through integrity types and verified assembly
• Representing object code
• Improved tool support for machine-code decompilation in HOL4
• Hoare Logic for ARM Machine Code
• Efficient substitution in Hoare logic expressions
• Hoare Logic for Realistically Modelled Machine Code
• Bidirectional grammars for machine-code decoding and encoding
• Simulation of operational semantics of machine instructions
• Automatic generation and validation of instruction encoders and decoders

Describes a project that uses

Uses Software

• Twelf
• ML

This page was built for publication: Machine instruction syntax and semantics in higher order logic

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