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

PCC Instantiation - Overflow & Type safety for SAL

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.

Machine Code: SAL Safety Policy: No overflows, No type errors Safety Logic: FOA (deep embedding)

Examples