Technische Universität München, Department of Computer Science, Chair IV: Software & Systems Engineering, Theorem Proving Group, VeryPCC Project


PCC Instantiation - Type safety for SAL

[empty] In these theories we instantiate our Proof Carrying Code Framework to a very simple assembly language (vSAL) with a safety policy that prohibits type errors. As safety logic we use Isabelle/HOL in form of a shallow embedding. From the framework we get a verified, executable VCG, which we use to certify the safety of vSAL programs. The safety proofs can be checked using Isabelle/HOL's proof checker. [empty]

Machine Code: downsized version of SAL
Safety Policy: No type errors
Safety Logic: Isabelle/HOL shallow embedding
[empty] [empty]
TermCodegen.thy [pdf] Extensions for Isabelle's ML program generator.
SALSemantics.thy [pdf] Syntax and semantics of SAL programs.
SALTypeSafetyPlatform.thy [pdf] Instantiates the VCG, a safety logic and a policy for type safety.
SALTypeSafetyFWInst.thy [pdf] Shows that this instantiation satisfies all requirements of the PCC Framework.


EX_Sum.thy [pdf] A program that adds the numbers from 0 to N.
Martin Wildmoser Last modified: Wed Jan 21 09:52:12 MET 2004