Certifying Machine Code Safety: Shallow versus Deep Embedding
We formalise a simple assembly language with procedures and a safety policy
for arithmetic overflow in Isabelle/HOL. To verify individual programs we
use a safety logic. Such a logic can be realised in Isabelle/HOL either as
shallow or deep embedding. In a shallow embedding logical formulas are
written as HOL predicates, whereas a deep embedding models formulas as a
datatype. This paper presents and discusses both variants pointing out
their specific strengths and weaknesses.
pdf (c) Springer Verlag
BibTeX:
@inproceedings{WildmoserN-TPHOLs04,
author={Martin Wildmoser and Tobias Nipkow},
title={Certifying Machine Code Safety: Shallow versus Deep Embedding},
booktitle={Theorem Proving in Higher Order Logics (TPHOLs 2004)},
editor={K. Slind and A. Bunker and G. Gopalakrishnan},
publisher=Springer,series=LNCS,volume=3223,pages={305-320},year=2004}