Publications by Kai Engelhardt (~) in reverse chronological order

[1]

Toby Murray, Robert Sison, and ~. Covern: A logic for compositional verification of information flow control. In Frank Piessens and Matthew Smith, editors, IEEE European Symposium on Security and Privacy (EuroS&P), April 2018. [ bib | DOI | .pdf | Abstract ]

[2]

~. A better composition operator for quantitative information flow analyses. In Simon N. Foley, Dieter Gollmann, and Einar Snekkenes, editors, Computer Security – ESORICS 2017, 22nd European Symposium on Research in Computer Security Oslo, Norway, September 11–15, 2017, Proceedings, Part I, volume 10492 of LNCS, pages 446–463, Oslo, Norway, September 11–13 2017. Springer-Verlag. [ bib | DOI | Abstract ]

[3]

Peter Gammie, Antony L. Hosking, and ~. Relaxing safely: Verified on-the-fly garbage collection for x86-TSO. In Steve Blackburn, editor, PLDI 2015, 36th annual ACM SIGPLAN conference on Programming Language Design and Implementation, pages 99–109, Portland, OR, May 2015. ACM. [ bib | Abstract ]

[4]

Peter Gammie, Tony Hosking, and ~. Relaxing safely: Verified on-the-fly garbage collection for x86-TSO. Archive of Formal Proofs, 2015. [ bib | http | Abstract ]

[5]

~, Ron van der Meyden, and Chenyi Zhang. Intransitive noninterference in nondeterministic systems. In Ting Yu, George Danezis, and Virgil D. Gligor, editors, 19th ACM Conference on Computer and Communications Security. ACM, October 2012. [ bib | Abstract ]

[6]

Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, ~, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: Formal verification of an operating-system kernel. Communications of the ACM, 53(6):107–115, June 2010. [ bib | DOI | Abstract ]

[7]

~. A note on noninterference in the presence of colluding adversaries (preliminary report). Presented at Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security, ARSPA-WITS'10, March 27–28 2010. [ bib | Abstract ]

[8]

~ and Ralf Huuck. Smaller abstractions for ∀CTL^* without Next. In Dennis Dams, Ulrich Hannemann, and Martin Steffen, editors, Concurrency, Compositionality, and Correctness: Essays in Honor of Willem-Paul de Roever, volume 5930 of LNCS, pages 250–259. Springer-Verlag, 2010. [ bib | Abstract ]

[9]

Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, ~, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: Formal verification of an OS kernel. In Proceedings of the 22nd ACM Symposium on Operating Systems Principles (SOSP), pages 207–220, Big Sky, MT, USA, October 2009. ACM. [ bib | PDF ]

[10]

~ and Yoram Moses. Causing communication closure: safe program composition with reliable non-FIFO channels. Distributed Computing, 22(2):73–91, October 2009. [ bib | DOI | Abstract ]

[11]

~ and Yoram Moses. Single-bit messages are insufficient for data link over duplicating channels. Information Processing Letters, 107(6):235–239, August 2008. [ bib | DOI | Abstract ]

[12]

~, Peter Gammie, and Ron van der Meyden. Model checking knowledge and linear time: PSPACE cases. In Sergei N. Artëmov and Anil Nerode, editors, Logical Foundations of Computer Science, International Symposium, LFCS 2007, New York, NY, USA, June 4-7, 2007, Proceedings, volume 4514 of LNCS, pages 195–211. Springer-Verlag, June 2007. [ bib | Abstract ]

[13]

~ and Yoram Moses. Single-bit messages are insufficient in the presence of duplication. In Ajit Pal, Ajay Kshemkalyani, Rajeev Kumar, and Arobinda Gupta, editors, 7th International Workshop on Distributed Computing IWDC 2005, volume 3741 of LNCS, pages 25–31. Springer-Verlag, December 27–30 2005. [ bib | DOI | Abstract ]

[14]

~ and Yoram Moses. Safe composition of distributed programs communicating over order-preserving imperfect channels. In Ajit Pal, Ajay Kshemkalyani, Rajeev Kumar, and Arobinda Gupta, editors, 7th International Workshop on Distributed Computing IWDC 2005, volume 3741 of LNCS, pages 32–44. Springer-Verlag, December 27–30 2005. [ bib | DOI | Abstract ]

[15]

~ and Yoram Moses. Causing communication closure: Safe program composition with non-FIFO channels. In Pierre Fraigniaud, editor, DISC 2005 19th International Symposium on Distributed Computing, volume 3724 of LNCS, pages 229–243. Springer-Verlag, September 26–29 2005. [ bib | DOI | Abstract ]

[16]

~, Ron van der Meyden, and Kaile Su. Modal logics with a linear hierarchy of local propositional quantifiers. In Philippe Balbiani, Nobu-Yuki Suzuki, Frank Wolter, and Michael Zakharyaschev, editors, Advances in Modal Logic, volume 4, pages 9–30. King's College London Publications, 2003. [ bib | Abstract ]

[17]

~, Ron van der Meyden, and Kaile Su. Modal logics with a linear hierarchy of local propositional quantifiers (preliminary version). In Nobu-Yuki Suzuki and Frank Wolter, editors, Advances in Modal Logic 2002 (AiML), pages 63–76. Institut de recherche en informatique de Toulouse, Université Paul Sabatier, September 2002. [ bib ]

[18]

~. Towards a refinement theory that supports reasoning about knowledge and time for multiple agents (work in progress). In John Derrick, Eerke Boiten, Jim Woodcock, and Joakim von Wright, editors, REFINE '02 An FME sponsored Refinement Workshop in collaboration with BCS FACS, page 23. Computing Laboratory, University of Kent at Canterbury, UK, July 2002. Preliminary Proceedings. [ bib ]

[19]

~, Ron van der Meyden, and Yoram Moses. A refinement theory that supports reasoning about knowledge and time for synchronous agents. In Robert Nieuwenhuis and Andrei Voronkov, editors, Proceedings LPAR 2001, volume 2250 of LNAI, pages 125–141. Springer-Verlag, December 2001. [ bib | DOI | Abstract ]

[20]

~, Ron van der Meyden, and Yoram Moses. A program refinement framework supporting reasoning about knowledge and time. In Jerzy Tiuryn, editor, Foundations of Software Science and Computation Structures, volume 1784 of LNCS, pages 114–129. Springer-Verlag, March 2000. [ bib | Abstract ]

[21]

~ and Ron van der Meyden. Modal logics with a hierarchy of local propositional quantifiers (extended abstract). In Thomas Eiter, Georg Gottlob, Victor Marek, and Jeffrey Remmel, editors, Proceedings of the FLoC'99 Workshop Complexity-Theoretic and Recursion-Theoretic Methods in Databases and Artificial Intelligence, pages 81–90, July 6 1999. [ bib ]

[22]

~, Ron van der Meyden, and Yoram Moses. Knowledge and the logic of local propositions. In Itzhak Gilboa, editor, Theoretical Aspects of Rationality and Knowledge, Proceedings of the Seventh Conference (TARK 1998), pages 29–41. Morgan Kaufmann, July 1998. [ bib | Abstract ]

[23]

Willem-Paul de Roever and ~. Data Refinement: Model-Oriented Proof Methods and their Comparison. Number 47 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1998. Paperback re-issue 2009. Errata at https://kai-e.github.io/pubs/dRE1998/errata.pdf. [ bib ]

[24]

~. Model-Oriented Data Refinement. PhD thesis, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel, July 1997. [ bib | Abstract ]

[25]

~ and Willem-Paul de Roever. New win[e/d] for old bags. In John Tromp, editor, A dynamic and quick intellect, Paul Vitányi 25 years @ CWI, pages 59–66. CWI, Amsterdam, November 1996. [ bib ]

[26]

~ and Willem-Paul de Roever. Simulation of specification statements in Hoare logic. In Wojciech Penczek and Andrzej Szalas, editors, Mathematical Foundations of Computer Science 1996, 21st International Symposium, MFCS '96, Cracow, Poland, Proceedings, volume 1113 of LNCS, pages 324–335. Springer-Verlag, September 1996. [ bib | Abstract ]

[27]

~ and Willem-Paul de Roever. Towards a practitioners' approach to Abadi and Lamport's method. Formal Aspects of Computing, 7(5):550–575, 1995. [ bib | Abstract ]

[28]

~ and Willem-Paul de Roever. Generalizing Abadi & Lamport's method to solve a problem posed by A. Pnueli. In Jim C.P. Woodcock and Peter Gorm Larsen, editors, FME '93: Industrial-Strength Formal Methods, volume 670 of LNCS, pages 294–313. Springer-Verlag, April 1993. [ bib ]

[29]

~. Verallgemeinerungen der Methode von Abadi und Lamport um ein von A. Pnueli gestelltes Problem zu lösen. Master's thesis, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel, January 1993. [ bib | Abstract ]