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 a variant of first order arithmetics in form of a deep embedding. Safety Proofs can be conducted in Isabelle using the Isabelle/HOL inference rules. 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. 


SALSyntax.thy [pdf]  Simple Assembly Language (SAL) instructions and datatypes. 
FiniteMap.thy [pdf]  Finite Maps are use for substitution functions. 
DeepLogic.thy [pdf]  Syntax (dataype form) and manipulation of formulae (substitution functions). 
SALSemantics_deep.thy [pdf]  The meaning of SAL programs in form of a small step semantics. 
SALSafetyLogic_deep.thy [pdf]  Instantiates the safety logic (connectives, judgements), the safety policy (safeF), and VCG parameter functions (succsF, wpF). 
SALOverflowPlatform.thy [pdf]  Instantiates the VCG and a wellformedness checker for SAL programs. 
SALOverflowFWInst.thy [pdf]  Shows that all instantiations satisfy the requirements of the PCC Framework. Establishes the VCG Soundness theorem for this platform. 
VCOpt.thy [pdf]  Defines and verifies an optimizer for verification conditions. 
EX_DoubleAddition_deep.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_RecMult_deep.thy [pdf]  Multiplies two numbers with a recursive procedure; uses pointers to simulate a call stack in memory. 
Martin Wildmoser  Last modified: Mon Jan 19 18:52:40 MET 2004 