Certifying Machine Code Safety: Shallow Versus Deep Embedding
Authors:
- 1 January 2004
- book chapter
- Published by Springer Nature
- p. 305-320
Abstract
No abstract availableKeywords
This publication has 11 references indexed in Scilit:
- Secure mechanical verification of mutually recursive proceduresInformation and Computation, 2003
- A syntactic approach to foundational proof-carrying code2003
- A provably sound TAL for back-end optimization2003
- Program Extraction in Simply-Typed Higher Order Logic2003
- Foundational proof-carrying code2002
- Isabelle/HOL2002
- Executing Higher Order Logic2002
- A certifying compiler for Java2000
- A semantic model of types and machine instructions for proof-carrying code2000
- Proof Terms for Simply Typed Higher Order Logic2000