Prototyping Proof Carrying Code

Martin Wildmoser, Tobias Nipkow, Gerwin Klein, Sebastian Nanz

We introduce a generic framework for proof carrying code, developed and mechanically verified in Isabelle/HOL. The framework defines and proves sound a verification condition generator with minimal assumptions on the underlying programming language, safety policy, and safety logic. We demonstrate its usability for prototyping proof carrying code systems by instantiating it to a simple assembly language with procedures and a safety policy for arithmetic overflow.



author={Martin Wildmoser and Tobias Nipkow and Gerwin Klein and Sebastian Nanz},
title={Prototyping Proof Carrying Code},
booktitle={Exploring New Frontiers of Theoretical Informatics},
editor={J.-J. Levy and E. Mayer and J. Mitchell},