peteg's webspace - papers
You can find BibTeX entries and so forth
- Verified Synthesis of Knowledge-Based
Programs in Finite Synchronous Environments, Interactive Theorem Proving (2011).
- seL4 Enforces Integrity, Interactive
Theorem Proving (2011) (with Thomas Sewell, Simon
Winwood, Toby Murray, June Andronick and Gerwin
- Provable Security: How Feasible Is It?,
USENIX HOTOS XIII (2011) (with Gerwin Klein, Toby Murray,
Thomas Sewell, and Simon Winwood).
- Short note: Strict unwraps make
worker/wrapper fusion totally correct, Journal of
Functional Programming 21(2): 209-213 (2011).
- Model Checking Knowledge and Linear Time:
PSPACE Cases, LFCS (2007) (with Kai Engelhardt and
Ron van der Meyden).
- MCK: Model Checking
the Logic of Knowledge, CAV (2004) (with Ron van der
The following are available at
of Formal Proofs: