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.

Online Copy

Available as [PDF]

Bibtex entry

  author="Martin Wildmoser and Tobias Nipkow and Gerwin Klein and Sebastian Nanz",
  title="Prototyping Proof Carrying Code",
  booktitle="Proc.\ TCS 3rd Int.\ Conf.\ on Theoretical Computer Science (TCS2004)",
  publisher="Kluwer Academic Publishers",
  editor="Jean-Jacques Levy and Ernst W. Mayr and John C. Mitchell",
Gerwin Klein
2005-02-18 16:29:04