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

PCC Instantiation - Bounded Runtime

In these theories we extend our SALOverflow instantiation with a safety policy that regards programs as safe if their runtime is bounded by a system constant MAXTIME. 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 Runtime, No overflows, No type errors Safety Logic: HOL (shallow embedding)

Examples