| 2017 | ESORICS | A Better Composition Operator for Quantitative Information Flow Analyses. | Kai Engelhardt |
| 2015 | PLDI | Relaxing safely: verified on-the-fly garbage collection for x86-TSO. | Peter Gammie, Antony L. Hosking, Kai Engelhardt |
| 2012 | CCS | Intransitive noninterference in nondeterministic systems. | Kai Engelhardt, Ron van der Meyden, Chenyi Zhang |
| 2009 | SOSP | seL4: formal verification of an OS kernel. | Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David A. Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, Simon Winwood |
| 2007 | LFCS | Model Checking Knowledge and Linear Time: PSPACE Cases. | Kai Engelhardt, Peter Gammie, Ron van der Meyden |
| 2002 | AiML | Modal Logics with a Linear Hierarchy of Local Propositional Quantifiers. | Kai Engelhardt, Ron van der Meyden, Kaile Su |
| 2001 | LPAR | A Refinement Theory that Supports Reasoning About Knowledge and Time. | Kai Engelhardt, Ron van der Meyden, Yoram Moses |
| 2000 | FOSSACS | A Program Refinement Framework Supporting Reasoning about Knowledge and Time. | Kai Engelhardt, Ron van der Meyden, Yoram Moses |
| 1998 | TARK | Knowledge and the Logic of Local Propositions. | Kai Engelhardt, Ron van der Meyden, Yoram Moses |
| 1996 | MFCS | Simulation of Specification Statements in Hoare Logic. | Kai Engelhardt, Willem P. de Roever |
| 1993 | FM | Generalizing Abadi & Lamport's Method to Solve a Problem Posed by A. Pnueli. | Kai Engelhardt, Willem P. de Roever |