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

[empty]

PCC Instantiation - Bounded Memory


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

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


Examples

EX_RecMultMem.thy [pdf] Multiplies two variables.
EX_ListRev.thy [pdf] Reverses a pointer list (without additional memory).
[empty]
Martin Wildmoser Last modified: Wed Jan 21 14:07:15 CET 2004