Technische Universität München, Department of Computer Science, Chair IV: Software & Systems Engineering, Theorem Proving Group, VeryPCC Project
In these theories we instantiate our Proof Carrying Code Framework to a simple assembly language (SAL) with a safety policy that prohibits arithmetic overflows and 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 various SAL programs. The safety proofs can be checked using Isabelle/HOL's proof checker. 


TermCodegen.thy [pdf]  Extensions for Isabelle's ML program generator. 
TupleOrd.thy [pdf]  Lexical ordering of pairs. 
SALSyntax.thy [pdf]  Simple Assembly Language (SAL) instructions and datatypes. 
SALSemantics.thy [pdf]  A formal semantics for SAL programs. 
SALSafetyLogic.thy [pdf]  HOL predicates as annotations (shallow embedding), logical operators for the safety logic 
SALOverflowPlatform.thy [pdf]  Instantiates the VCG and a safety policy that prohibits arithmetic overflows and type errors. 
SALOverflowFWInst.thy [pdf]  Shows that this instantiation satisfies all requirements of the PCC Framework. 
EX_DoubleAddition.thy [pdf]  Very primitive example: Computes 4 times X using two additions. 
EX_SmartCardPurse.thy [pdf]  A check procedure protects the balance of a smart card purse from overflows. 
EX_SmartCardPurse_fa.thy [pdf]  Same example as above, except that we use more annotations here. 
EX_RecMult.thy [pdf]  Multiplies two numbers with a recursive procedure; uses pointers to simulate a call stack in memory. 
Martin Wildmoser  Last modified: Mon Jan 12 19:48:22 MET 2004 