Follow
Kai Engelhardt
Kai Engelhardt
n.a.
Verified email at acm.org
Title
Cited by
Cited by
Year
seL4: Formal verification of an OS kernel
G Klein, K Elphinstone, G Heiser, J Andronick, D Cock, P Derrin, ...
Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles …, 2009
27622009
Data Refinement: Model-oriented proof methods and their comparison
WP de Roever, K Engelhardt
Cambridge University Press, 1998
5941998
Knowledge and the logic of local propositions
K Engelhardt, R van der Meyden, Y Moses
Proceedings of the 7th conference on Theoretical aspects of rationality and …, 1998
761998
COVERN: A logic for compositional verification of information flow control
T Murray, R Sison, K Engelhardt
2018 IEEE European Symposium on Security and Privacy (EuroS&P), 16-30, 2018
422018
Relaxing safely: verified on-the-fly garbage collection for x86-TSO
P Gammie, AL Hosking, K Engelhardt
ACM SIGPLAN Notices 50 (6), 99-109, 2015
342015
Model checking knowledge and linear time: PSPACE cases
K Engelhardt, P Gammie, R Van Der Meyden
Logical Foundations of Computer Science: International Symposium, LFCS 2007 …, 2007
202007
A program refinement framework supporting reasoning about knowledge and time
K Engelhardt, R van der Meyden, Y Moses
Foundations of Software Science and Computation Structures, 114-129, 2000
192000
A refinement theory that supports reasoning about knowledge and time for synchronous agents
K Engelhardt, R van der Meyden, Y Moses
International Conference on Logic for Programming Artificial Intelligence …, 2001
182001
Intransitive noninterference in nondeterministic systems
K Engelhardt, R Van Der Meyden, C Zhang
Proceedings of the 2012 ACM conference on Computer and communications …, 2012
162012
Modal Logics with a Linear Hierarchy of Local Propositional Quantifiers (Preliminary Report)
K Engelhardt, R van der Meyden, K Su
16*
Generalizing Abadi & Lamport's method to solve a problem posed by A. Pnueli
K Engelhardt, WP de Roever
International Symposium of Formal Methods Europe, 294-313, 1993
91993
Safe composition of distributed programs communicating over order-preserving imperfect channels
K Engelhardt, Y Moses
International Workshop on Distributed Computing, 32-44, 2005
82005
Single-bit messages are insufficient in the presence of duplication
K Engelhardt, Y Moses
International Workshop on Distributed Computing, 25-31, 2005
62005
Model-oriented data refinement
K Engelhardt
Christian-Albrechts-Universität zu Kiel, 1997
61997
Simulation of specification statements in Hoare logic
K Engelhardt, WP de Roever
International Symposium on Mathematical Foundations of Computer Science, 324-335, 1996
51996
Causing communication closure: safe program composition with reliable non-FIFO channels
K Engelhardt, Y Moses
Distributed Computing 22 (2), 73-91, 2009
32009
A better composition operator for quantitative information flow analyses
K Engelhardt
Computer Security–ESORICS 2017: 22nd European Symposium on Research in …, 2017
22017
Causing communication closure: Safe program composition with non-FIFO channels
K Engelhardt, Y Moses
International Symposium on Distributed Computing, 229-243, 2005
22005
Towards a practitioners' approach to Abadi and Lamport's method
K Engelhardt, WP de Roever
Formal aspects of computing 7, 550-575, 1995
21995
Single-bit messages are insufficient for data link over duplicating channels
K Engelhardt, Y Moses
Information processing letters 107 (6), 235-239, 2008
12008
The system can't perform the operation now. Try again later.
Articles 1–20