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

PCC Instantiation - Bounded Memory

In these theories we extend our SALOverflow instantiation with a safety policy that regards programs as safe if they do not use memory above address MAXMEM. In addition programs must be type safe and free of arithmetic overflows as the original safety policy demands. Safety Logic and programming lanuage SAL are the same as in SALOverflow instantiation.

Machine Code: SAL Safety Policy: Bounded Memory, No overflows, No type errors Safety Logic: HOL (shallow embedding)

Examples