A Proof-Carrying Code Architecture for Java
Abstract elided by the publisher.
Related papers
- A machine-checked model for a Java-like language, virtual machine, and compiler TOPLAS 2006
- A certifying compiler for Java PLDI 2000
- Oracle-based checking of untrusted software POPL 2001
- Proof-Carrying Code in a Session-Typed Process Calculus CPP 2011
- What Are We Trying to Prove? Reflections on Experiences with Proof-Carrying Code TACAS 2003
- A Semantic Model of Types and Machine Instructions for Proof-Carrying Code POPL 2000
- Proof-Carrying Code POPL 1997
- An indexed model of recursive types for foundational proof-carrying code TOPLAS 2001