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

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.

Machine Code: downsized version of SAL Safety Policy: No type errors Safety Logic: Isabelle/HOL shallow embedding

Examples