peteg's webspace - papers
You can find BibTeX entries and so forth
at DBLP. My thesis
work may also be of interest.
- Relaxing safely: verified on-the-fly
garbage collection for x86-TSO, ACM PLDI (2015) (with Tony
Hosking and Kai Engelhardt).
- Synchronous digital circuits as functional
programs, ACM Computing Surveys (2013).
- seL4: from General Purpose to a Proof of
Information Flow Enforcement, IEEE Symposium on
Security and Privacy (2013) (with Toby Murray, Daniel
Matichuk, Matthew Brassil, Timothy Bourke, Sean Seefried,
Corey Lewis, Xin Gao and Gerwin Klein).
- Noninterference for Operating System
Kernels, The Second International Conference on
Certified Programs and Proofs (2012) (with Toby Murray,
Daniel Matichuk, Matthew Brassil and Gerwin Klein).
- 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: