@inproceedings{f895e9087ed74f0893ea1291ccc8bd71,
title = "Machine instruction syntax and semantics in higher order logic",
abstract = "Proof-carrying code and other applications in computer security require machine-checkable proofs of properties of machine-language programs. These in turn require axioms about the opcode/operand encoding of machine instructions and the semantics of the encoded instructions. We show how to specify instruction encodings and semantics in higher-order logic, in a way that preserves the factoring of similar instructions in real machine architectures. We show how to automatically generate proofs of instruction decodings, global invariants from local invariants, Floyd-Hoare rules and predicate transformers, all from the specification of the instruction semantics. Our work is implemented in ML and Twelf, and all the theorems are checked in Twelf.",
author = "Michael, {Neophytos G.} and Appel, {Andrew W.}",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 2000.; 17th International Conference on Automated Deduction, CADE 2000 ; Conference date: 17-06-2000 Through 20-06-2000",
year = "2000",
doi = "10.1007/10721959_2",
language = "English (US)",
series = "Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science)",
publisher = "Springer Verlag",
pages = "7--24",
editor = "David McAllester",
booktitle = "Automated Deduction - CADE-17 - 17th International Conference on Automated Deduction, Proceedings",
address = "Germany",
}