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


PCC Instantiation - Bounded Runtime

[empty] 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. [empty]

Machine Code: SAL
Safety Policy: Bounded Runtime, No overflows, No type errors
Safety Logic: HOL (shallow embedding)
[empty] [empty]
SALTimePlatform.thy [pdf] Extends SALOverflowPlatform.thy to a new safety policy, and instantiates the VCG with it.
SALTimeFWInst.thy [pdf] Verifies that this instantiation satisfies the requirements of the PCCFramework und thus guarantees the soundness of this PCC Platform.


EX_Mult.thy [pdf] A machine program that multiplies two variables.
Martin Wildmoser Last modified: Tue Jan 13 13:41:21 MET 2004