Generalizing Abadi & Lamport's Method to Solve a Problem Posed by A. Pnueli. - Kai Engelhardt; Willem P. de Roever (FME, 1993)

Towards a Practitioners' Approach to Abadi and Lamport's Method. - Kai Engelhardt; Willem P. de Roever (Formal Aspects Comput., 1995)

Simulation of Specification Statements in Hoare Logic. - Kai Engelhardt; Willem P. de Roever (MFCS, 1996)

Model oriented data refinement. - Kai Engelhardt (1997)

Data Refinement: Model-oriented Proof Theories and their Comparison - Willem P. de Roever; Kai Engelhardt (Cambridge University Press, 1998)

Knowledge and the Logic of Local Propositions. - Kai Engelhardt; Ron van der Meyden; Yoram Moses (TARK, 1998)

A Program Refinement Framework Supporting Reasoning about Knowledge and Time. - Kai Engelhardt; Ron van der Meyden; Yoram Moses (FoSSaCS, 2000)

A Refinement Theory that Supports Reasoning About Knowledge and Time. - Kai Engelhardt; Ron van der Meyden; Yoram Moses (LPAR, 2001)

Modal Logics with a Linear Hierarchy of Local Propositional Quantifiers. - Kai Engelhardt; Ron van der Meyden; Kaile Su (Advances in Modal Logic, 2002)

Towards a refinement theory that supports reasoning about knowledge and time for multiple agents. - Kai Engelhardt (Refine, 2002)

Single-Bit Messages Are Insufficient in the Presence of Duplication. - Kai Engelhardt; Yoram Moses (IWDC, 2005)

Safe Composition of Distributed Programs Communicating over Order-Preserving Imperfect Channels. - Kai Engelhardt; Yoram Moses (IWDC, 2005)

Causing Communication Closure: Safe Program Composition with Non-FIFO Channels. - Kai Engelhardt; Yoram Moses (DISC, 2005)

Model Checking Knowledge and Linear Time: PSPACE Cases. - Kai Engelhardt; Peter Gammie; Ron van der Meyden (LFCS, 2007)

Single-bit messages are insufficient for data link over duplicating channels. - Kai Engelhardt; Yoram Moses (Inf. Process. Lett., 2008)

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; et al. (SOSP, 2009)

Causing communication closure: safe program composition with reliable non-FIFO channels. - Kai Engelhardt; Yoram Moses (Distributed Comput., 2009)

Smaller Abstractions for FOR ALL CTL* without Next. - Kai Engelhardt; Ralf Huuck (Concurrency, Compositionality, and Correctness, 2010)

seL4: formal verification of an operating-system kernel. - Gerwin Klein; June Andronick; Kevin Elphinstone; Gernot Heiser; David A. Cock; Philip Derrin; Dhammika Elkaduwe; Kai Engelhardt; Rafal Kolanski; Michael Norrish; Thomas Sewell; Harvey Tuch; et al. (Commun. ACM, 2010)

Intransitive noninterference in nondeterministic systems. - Kai Engelhardt; Ron van der Meyden; Chenyi Zhang 001 (CCS, 2012)

Relaxing Safely: Verified On-the-Fly Garbage Collection for x86-TSO. - Peter Gammie; Tony Hosking; Kai Engelhardt (Arch. Formal Proofs, 2015)

A Better Composition Operator for Quantitative Information Flow Analyses. - Kai Engelhardt (ESORICS (1), 2017)

COVERN: A Logic for Compositional Verification of Information Flow Control. - Toby C. Murray; Robert Sison; Kai Engelhardt (EuroS&P, 2018)