Kai Engelhardt

25 papers A* 3A 2B 5Misc 1Journal 6Unranked 6
YearRankTypeTitle / Venue / Authors
2018 A conf
COVERN: A Logic for Compositional Verification of Information Flow Control.
EuroS&P
Toby C. Murray, Robert Sison, Kai Engelhardt
2017 — conf
A Better Composition Operator for Quantitative Information Flow Analyses.
ESORICS (1)
Kai Engelhardt
2015 J jnl
Relaxing Safely: Verified On-the-Fly Garbage Collection for x86-TSO.
Arch. Formal Proofs
Peter Gammie, Tony Hosking, Kai Engelhardt
2015 A* conf
Relaxing safely: verified on-the-fly garbage collection for x86-TSO.
PLDI
Peter Gammie, Antony L. Hosking, Kai Engelhardt
2012 A* conf
Intransitive noninterference in nondeterministic systems.
CCS
Kai Engelhardt, Ron van der Meyden, Chenyi Zhang
2010 — conf
Smaller Abstractions for FOR ALL CTL* without Next.
Concurrency, Compositionality, and Correctness
Kai Engelhardt, Ralf Huuck
2010 J jnl
seL4: formal verification of an operating-system kernel.
Commun. ACM
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, Simon Winwood
2009 J jnl
Causing communication closure: safe program composition with reliable non-FIFO channels.
Distributed Comput.
Kai Engelhardt, Yoram Moses
2009 A* conf
seL4: formal verification of an OS kernel.
SOSP
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
2008 J jnl
Single-bit messages are insufficient for data link over duplicating channels.
Inf. Process. Lett.
Kai Engelhardt, Yoram Moses
2007 J jnl
Causing Communication Closure: Safe Program Composition with Reliable Non-FIFO Channels
CoRR
Kai Engelhardt, Yoram Moses
2007 Misc conf
Model Checking Knowledge and Linear Time: PSPACE Cases.
LFCS
Kai Engelhardt, Peter Gammie, Ron van der Meyden
2005 A conf
Causing Communication Closure: Safe Program Composition with Non-FIFO Channels.
DISC
Kai Engelhardt, Yoram Moses
2005 — conf
Safe Composition of Distributed Programs Communicating over Order-Preserving Imperfect Channels.
IWDC
Kai Engelhardt, Yoram Moses
2005 — conf
Single-Bit Messages Are Insufficient in the Presence of Duplication.
IWDC
Kai Engelhardt, Yoram Moses
2002 B conf
Modal Logics with a Linear Hierarchy of Local Propositional Quantifiers.
Advances in Modal Logic
Kai Engelhardt, Ron van der Meyden, Kaile Su
2002 — conf
Towards a refinement theory that supports reasoning about knowledge and time for multiple agents.
Refine
Kai Engelhardt
2001 B conf
A Refinement Theory that Supports Reasoning About Knowledge and Time.
LPAR
Kai Engelhardt, Ron van der Meyden, Yoram Moses
2000 B conf
A Program Refinement Framework Supporting Reasoning about Knowledge and Time.
FoSSaCS
Kai Engelhardt, Ron van der Meyden, Yoram Moses
1998 — book
Data Refinement: Model-oriented Proof Theories and their Comparison
Willem P. de Roever, Kai Engelhardt
1998 B conf
Knowledge and the Logic of Local Propositions.
TARK
Kai Engelhardt, Ron van der Meyden, Yoram Moses
1997 — —
Model oriented data refinement.
Kai Engelhardt
1996 B conf
Simulation of Specification Statements in Hoare Logic.
MFCS
Kai Engelhardt, Willem P. de Roever
1995 J jnl
Towards a Practitioners' Approach to Abadi and Lamport's Method.
Formal Aspects Comput.
Kai Engelhardt, Willem P. de Roever
1993 — conf
Generalizing Abadi & Lamport's Method to Solve a Problem Posed by A. Pnueli.
FME
Kai Engelhardt, Willem P. de Roever