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


PCC Framework

[empty] Proof Carrying Code (PCC) systems are determined by three factors: the programming language, the safety policy and the safety logic. In this framework we identify the key functions and requirements for these three and construct and verify a generic Verification Condition Generator (VCG). If one can prove the formula it produces for an annotated program, the safety of this program is guaranteed. The generic VCG can be instantiated to various PCC systems by defining the functions it takes as parameters. Using Isabelle's ML code generator one can extract an executable version of the VCG, which forms together with Isabelle's built in proof checker a running PCC system. [empty]

PCCFramework.thy [pdf] introduces just the chapter heading "PCC Framework".
Semantics.thy [pdf] defines a framework for program semantics.
SafetyLogic.thy [pdf] defines a framework for the safety logic.
AuxBox.thy [pdf] contains auxiliary functions for general purposes and theorems about those.
CFG.thy [pdf] defines control flow graphs.
AbsSem.thy [pdf] defines functions for an abstract program semantics.
VCG.thy [pdf] defines the generic Verification Condition Generator (VCG).
VCG_Correctness.thy [pdf] Correctness of the VCG: Provable verification conditions imply program safety!
VCG_Completeness.thy [pdf] Completeness of the VCG. Under what conditions are verification conditions tautologies?
VCG_Invariant.thy [pdf] Completeness of the VCG. Under what conditions are verification conditions invariants?
VCG_Upgrades.thy [pdf] Theorems to upgrade instantiations of these frameworks.
Martin Wildmoser Last modified: Wed Jan 18 17:43:14 MET 2006