| Publication | Date of Publication | Type |
|---|
| A rely-guarantee-based simulation for cooperative semantics | 2026-03-20 | Paper |
Cogent: uniqueness types and certifying compilation
Journal of Functional Programming | 2021-12-27 | Paper |
Formal reasoning under cached address translation
Journal of Automated Reasoning | 2020-11-02 | Paper |
Reasoning about Translation Lookaside Buffers
EPiC Series in Computing | 2019-01-10 | Paper |
| Backwards and forwards with separation logic | 2018-10-04 | Paper |
| Program verification in the presence of cached address translation | 2018-10-04 | Paper |
Refinement through restraint: bringing down the cost of verification
Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming | 2017-05-10 | Paper |
A framework for the automatic formal verification of refinement from \textsc{Cogent} to C
Interactive Theorem Proving | 2016-10-27 | Paper |
Concerned with the unprivileged: user programs in kernel refinement
Formal Aspects of Computing | 2016-08-05 | Paper |
Experience report: seL4, formally verifying a high-performance microkernel
Proceedings of the 14th ACM SIGPLAN international conference on Functional programming | 2015-01-06 | Paper |
| Concrete semantics. With Isabelle/HOL | 2014-10-23 | Paper |
Types, bytes, and separation logic
Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2014-09-12 | Paper |
Noninterference for operating system kernels
Certified Programs and Proofs | 2013-04-19 | Paper |
Bridging the Gap: Automatic Verified Abstraction of C
Interactive Theorem Proving | 2012-09-20 | Paper |
Mechanised Separation Algebra
Interactive Theorem Proving | 2012-09-20 | Paper |
Challenges and experiences in managing large-scale proofs
Lecture Notes in Computer Science | 2012-09-07 | Paper |
seL4 enforces integrity
Interactive Theorem Proving | 2011-08-17 | Paper |
Operating system verification---an overview
Sādhanā | 2009-11-23 | Paper |
Types, Maps and Separation Logic
Lecture Notes in Computer Science | 2009-10-20 | Paper |
Secure Microkernels, State Monads and Scalable Refinement
Lecture Notes in Computer Science | 2008-12-04 | Paper |
A Unified Memory Model for Pointers
Logic for Programming, Artificial Intelligence, and Reasoning | 2008-05-27 | Paper |
On the Automated Synthesis of Proof-Carrying Temporal Reference Monitors
Logic-Based Program Synthesis and Transformation | 2007-09-10 | Paper |
| scientific article; zbMATH DE number 2163030 (Why is no real title available?) | 2005-04-29 | Paper |
Verified bytecode verification and type-certifying compilation
The Journal of Logic and Algebraic Programming | 2004-10-14 | Paper |
Verified bytecode subroutines
Journal of Automated Reasoning | 2003-09-09 | Paper |
Verified bytecode verifiers.
Theoretical Computer Science | 2003-05-25 | Paper |
Verified lightweight bytecode verification
Concurrency and Computation: Practice and Experience | 2002-05-01 | Paper |
