Select Publications

by Dr Kai Engelhardt

Books

de Roever W-P; Engelhardt K, 2009, Data Refinement: Model-Oriented Proof Methods and their Comparison, Paperback, Cambridge University Press, Cambridge, UK

Book Chapters

Engelhardt K; Huuck R, 2010, 'Smaller abstractions for ?CTL* without next*', in , pp. 250 - 259, http://dx.doi.org/10.1007/978-3-642-11512-7_16

Journal articles

Klein G; Andronick J; Elphinstone K; Heiser G; Cock D; Derrin P; Elkaduwe D; Engelhardt K; Kolanski R; Norrish M; Sewell T; Tuch H; Winwood S, 2010, 'SeL4: Formal verification of an operating-system kernel', Communications of the ACM, vol. 53, no. 6, pp. 107 - 115, http://dx.doi.org/10.1145/1743546.1743574

Engelhardt K; Moses Y, 2009, 'Causing communication closure: Safe program composition with reliable non-FIFO channels', Distributed Computing, vol. 22, no. 2, pp. 73 - 91, http://dx.doi.org/10.1007/s00446-009-0081-9

Engelhardt K; Moses Y, 2008, 'Single-bit messages are insufficient for data link over duplicating channels', Information Processing Letters, vol. 107, no. 6, pp. 235 - 239, http://dx.doi.org/10.1016/j.ipl.2008.03.010

Conference Papers

Engelhardt K; Van Der Meyden R; Zhang C, 2012, 'Intransitive noninterference in nondeterministic systems', in Proceedings of the ACM Conference on Computer and Communications Security, pp. 869 - 880, http://dx.doi.org/10.1145/2382196.2382288

Klein G; Elphinstone K; Heiser G; Andronick J; Cock D; Derrin P; Elkaduwe D; Engelhardt K; Kolanski R; Norrish M; Sewell T; Tuch H; Winwood S, 2009, 'SeL4: Formal verification of an OS kernel', in SOSP'09 - Proceedings of the 22nd ACM SIGOPS Symposium on Operating Systems Principles, pp. 207 - 220, http://dx.doi.org/10.1145/1629575.1629596

Engelhardt K; Gammie P; Van Der Meyden R, 2007, 'Model checking knowledge and linear time: PSPACE cases', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 195 - 211

Engelhardt K; Moses Y, 2005, 'Safe composition of distributed programs communicating over order-preserving imperfect channels', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 32 - 44

Engelhardt K; Moses Y, 2005, 'Causing communication closure: Safe program composition with non-FIFO channels', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 229 - 243, http://dx.doi.org/10.1007/11561927_18

Engelhardt K; Moses Y, 2005, 'Single-bit messages are insufficient in the presence of duplication', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 25 - 31

Engelhardt K; Van Der Meyden R, 2002, 'Modal Logics with a Linear Hierarchy of Local Propositional Quantifiers (Preliminary Version)', in Advances in Modal Logic 2002 (AiML), presented at Advances in Modal Logic 2002 (AiML), Toulouse France, 2 September 2002

Engelhardt K, 2002, 'Towards a Refinement Theory that Supports Reasoning about Knowledge and Time for Multiple Agents (Work in Progress)', in REFINE 2002, presented at REFINE `02, Copenhagen, Denmark, 20 - 21 July 2002

Engelhardt K; Van Der Meyden R; Moses Y, 2001, 'A refinement theory that supports reasoning about knowledge and time for synchronous agents', in Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science), Springer Verlag, pp. 125 - 141

Engelhardt K; Van Der Meyden R; Moses Y, 2000, 'A program refinement framework supporting reasoning about knowledge and time', in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), pp. 114 - 129

Conference Presentations

Engelhardt K, 2010, 'A note on noninterference in the presence of colluding adversaries (preliminary report)', 1 January 2010


Back to profile page