-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathkai-e-pubs.html
More file actions
467 lines (379 loc) · 14.7 KB
/
kai-e-pubs.html
File metadata and controls
467 lines (379 loc) · 14.7 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
<head>
<link rel="stylesheet" href="/assets/css/style.css">
</head>
<!-- This document was automatically generated with bibtex2html 1.99
(see http://www.lri.fr/~filliatr/bibtex2html/),
with the following command:
bibtex2html -both -s plain -nf HTTP "web site" -nf PDF PDF -nf PS PS -nokeywords -d -r -dl -nofooter -nodoc -html-entities -t "Publications by Kai Engelhardt (~) in reverse chronological order" kai-e-pubs.bib -->
<h1>Publications by Kai Engelhardt (~) in reverse chronological order</h1>
<dl>
<dt>
[<a name="MSE2018euroSnP">1</a>]
</dt>
<dd>
Toby Murray, Robert Sison, and ~.
Covern: A logic for compositional verification of
information flow control.
In Frank Piessens and Matthew Smith, editors, <em>IEEE European
Symposium on Security and Privacy (EuroS&P)</em>, April 2018.
[ <a href="kai-e-pubs_bib.html#MSE2018euroSnP">bib</a> |
<a href="http://dx.doi.org/10.1109/EuroSP.2018.00010">DOI</a> |
<a href="https://covern.org/papers/EuroSP18.pdf">.pdf</a> |
<a href="kai-e-pubs_abstracts.html#MSE2018euroSnP">Abstract</a> ]
</dd>
<dt>
[<a name="E2017qifca">2</a>]
</dt>
<dd>
~.
A better composition operator for quantitative information flow
analyses.
In Simon N. Foley, Dieter Gollmann, and Einar Snekkenes, editors,
<em>Computer Security – ESORICS 2017, 22nd European Symposium on Research
in Computer Security Oslo, Norway, September 11–15, 2017, Proceedings, Part
I</em>, volume 10492 of <em>LNCS</em>, pages 446–463, Oslo, Norway, September
11–13 2017. Springer-Verlag.
[ <a href="kai-e-pubs_bib.html#E2017qifca">bib</a> |
<a href="http://dx.doi.org/10.1007/978-3-319-66402-6_26">DOI</a> |
<a href="kai-e-pubs_abstracts.html#E2017qifca">Abstract</a> ]
</dd>
<dt>
[<a name="GHE2015:PLDI">3</a>]
</dt>
<dd>
Peter Gammie, Antony L. Hosking, and ~.
Relaxing safely: Verified on-the-fly garbage collection for
x86-TSO.
In Steve Blackburn, editor, <em>PLDI 2015, 36th annual ACM
SIGPLAN conference on Programming Language Design and Implementation</em>, pages
99–109, Portland, OR, May 2015. ACM.
[ <a href="kai-e-pubs_bib.html#GHE2015:PLDI">bib</a> |
<a href="kai-e-pubs_abstracts.html#GHE2015:PLDI">Abstract</a> ]
</dd>
<dt>
[<a name="GHE2015:afp">4</a>]
</dt>
<dd>
Peter Gammie, Tony Hosking, and ~.
Relaxing safely: Verified on-the-fly garbage collection for
x86-TSO.
<em>Archive of Formal Proofs</em>, 2015.
[ <a href="kai-e-pubs_bib.html#GHE2015:afp">bib</a> |
<a href="http://afp.sourceforge.net/entries/ConcurrentGC.shtml">http</a> |
<a href="kai-e-pubs_abstracts.html#GHE2015:afp">Abstract</a> ]
</dd>
<dt>
[<a name="EvdMZ2012a">5</a>]
</dt>
<dd>
~, Ron van der Meyden, and Chenyi Zhang.
Intransitive noninterference in nondeterministic systems.
In Ting Yu, George Danezis, and Virgil D. Gligor, editors, <em>19th
ACM Conference on Computer and Communications Security</em>. ACM, October 2012.
[ <a href="kai-e-pubs_bib.html#EvdMZ2012a">bib</a> |
<a href="kai-e-pubs_abstracts.html#EvdMZ2012a">Abstract</a> ]
</dd>
<dt>
[<a name="Klein_EH_10:cacm">6</a>]
</dt>
<dd>
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.
<em>Communications of the ACM</em>, 53(6):107–115, June 2010.
[ <a href="kai-e-pubs_bib.html#Klein_EH_10:cacm">bib</a> |
<a href="http://dx.doi.org/10.1145/1743546.1743574">DOI</a> |
<a href="kai-e-pubs_abstracts.html#Klein_EH_10:cacm">Abstract</a> ]
</dd>
<dt>
[<a name="E2010:ARSPA_WITS">7</a>]
</dt>
<dd>
~.
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.
[ <a href="kai-e-pubs_bib.html#E2010:ARSPA_WITS">bib</a> |
<a href="kai-e-pubs_abstracts.html#E2010:ARSPA_WITS">Abstract</a> ]
</dd>
<dt>
[<a name="EH2008">8</a>]
</dt>
<dd>
~ and Ralf Huuck.
Smaller abstractions for ∀CTL<sup>*</sup> without Next.
In Dennis Dams, Ulrich Hannemann, and Martin Steffen, editors, <em>
Concurrency, Compositionality, and Correctness: Essays in Honor of
Willem-Paul de Roever</em>, volume 5930 of <em>LNCS</em>, pages 250–259.
Springer-Verlag, 2010.
[ <a href="kai-e-pubs_bib.html#EH2008">bib</a> |
<a href="kai-e-pubs_abstracts.html#EH2008">Abstract</a> ]
</dd>
<dt>
[<a name="Klein_EH_09">9</a>]
</dt>
<dd>
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 <em>Proceedings of the 22nd ACM Symposium on Operating Systems
Principles (SOSP)</em>, pages 207–220, Big Sky, MT, USA, October 2009. ACM.
[ <a href="kai-e-pubs_bib.html#Klein_EH_09">bib</a> |
<a href="http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf">PDF</a> ]
</dd>
<dt>
[<a name="EM2009dc">10</a>]
</dt>
<dd>
~ and Yoram Moses.
Causing communication closure: safe program composition with reliable
non-FIFO channels.
<em>Distributed Computing</em>, 22(2):73–91, October 2009.
[ <a href="kai-e-pubs_bib.html#EM2009dc">bib</a> |
<a href="http://dx.doi.org/10.1007/s00446-009-0081-9">DOI</a> |
<a href="kai-e-pubs_abstracts.html#EM2009dc">Abstract</a> ]
</dd>
<dt>
[<a name="EM2008ipl">11</a>]
</dt>
<dd>
~ and Yoram Moses.
Single-bit messages are insufficient for data link over duplicating
channels.
<em>Information Processing Letters</em>, 107(6):235–239, August 2008.
[ <a href="kai-e-pubs_bib.html#EM2008ipl">bib</a> |
<a href="http://dx.doi.org/10.1016/j.ipl.2008.03.010">DOI</a> |
<a href="kai-e-pubs_abstracts.html#EM2008ipl">Abstract</a> ]
</dd>
<dt>
[<a name="EGvdM2007:LFCS">12</a>]
</dt>
<dd>
~, Peter Gammie, and Ron van der Meyden.
Model checking knowledge and linear time: PSPACE cases.
In Sergei N. Artëmov and Anil Nerode, editors, <em>Logical
Foundations of Computer Science, International Symposium, LFCS 2007, New
York, NY, USA, June 4-7, 2007, Proceedings</em>, volume 4514 of <em>LNCS</em>, pages
195–211. Springer-Verlag, June 2007.
[ <a href="kai-e-pubs_bib.html#EGvdM2007:LFCS">bib</a> |
<a href="kai-e-pubs_abstracts.html#EGvdM2007:LFCS">Abstract</a> ]
</dd>
<dt>
[<a name="EM2005c">13</a>]
</dt>
<dd>
~ and Yoram Moses.
Single-bit messages are insufficient in the presence of duplication.
In Ajit Pal, Ajay Kshemkalyani, Rajeev Kumar, and Arobinda Gupta,
editors, <em>7<sup></sup><em>th</em> International Workshop on Distributed Computing
IWDC 2005</em>, volume 3741 of <em>LNCS</em>, pages 25–31. Springer-Verlag,
December 27–30 2005.
[ <a href="kai-e-pubs_bib.html#EM2005c">bib</a> |
<a href="http://dx.doi.org/10.1007/11603771_3">DOI</a> |
<a href="kai-e-pubs_abstracts.html#EM2005c">Abstract</a> ]
</dd>
<dt>
[<a name="EM2005b">14</a>]
</dt>
<dd>
~ 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, <em>7<sup></sup><em>th</em> International Workshop on Distributed Computing
IWDC 2005</em>, volume 3741 of <em>LNCS</em>, pages 32–44. Springer-Verlag,
December 27–30 2005.
[ <a href="kai-e-pubs_bib.html#EM2005b">bib</a> |
<a href="http://dx.doi.org/10.1007/11603771_4">DOI</a> |
<a href="kai-e-pubs_abstracts.html#EM2005b">Abstract</a> ]
</dd>
<dt>
[<a name="EM2005a">15</a>]
</dt>
<dd>
~ and Yoram Moses.
Causing communication closure: Safe program composition with
non-FIFO channels.
In Pierre Fraigniaud, editor, <em>DISC 2005 19<sup></sup><em>th</em>
International Symposium on Distributed Computing</em>, volume 3724 of <em>LNCS</em>,
pages 229–243. Springer-Verlag, September 26–29 2005.
[ <a href="kai-e-pubs_bib.html#EM2005a">bib</a> |
<a href="http://dx.doi.org/10.1007/11561927_18">DOI</a> |
<a href="kai-e-pubs_abstracts.html#EM2005a">Abstract</a> ]
</dd>
<dt>
[<a name="EvdMS:AiMLbook">16</a>]
</dt>
<dd>
~, 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, <em>Advances in Modal Logic</em>, volume 4, pages 9–30.
King's College London Publications, 2003.
[ <a href="kai-e-pubs_bib.html#EvdMS:AiMLbook">bib</a> |
<a href="kai-e-pubs_abstracts.html#EvdMS:AiMLbook">Abstract</a> ]
</dd>
<dt>
[<a name="EvdMS2002:AiML">17</a>]
</dt>
<dd>
~, 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, <em>Advances in Modal
Logic 2002 (AiML)</em>, pages 63–76. Institut de recherche en informatique de
Toulouse, Université Paul Sabatier, September 2002.
[ <a href="kai-e-pubs_bib.html#EvdMS2002:AiML">bib</a> ]
</dd>
<dt>
[<a name="E2002:Refine">18</a>]
</dt>
<dd>
~.
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, <em>REFINE '02 An FME sponsored Refinement Workshop in
collaboration with BCS FACS</em>, page 23. Computing Laboratory, University of
Kent at Canterbury, UK, July 2002.
Preliminary Proceedings.
[ <a href="kai-e-pubs_bib.html#E2002:Refine">bib</a> ]
</dd>
<dt>
[<a name="EvdMM2001:LPAR">19</a>]
</dt>
<dd>
~, 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, <em>Proceedings
LPAR 2001</em>, volume 2250 of <em>LNAI</em>, pages 125–141. Springer-Verlag,
December 2001.
[ <a href="kai-e-pubs_bib.html#EvdMM2001:LPAR">bib</a> |
<a href="http://dx.doi.org/10.1007/3-540-45653-8_9">DOI</a> |
<a href="kai-e-pubs_abstracts.html#EvdMM2001:LPAR">Abstract</a> ]
</dd>
<dt>
[<a name="EvdMM2000:FOSSACS">20</a>]
</dt>
<dd>
~, Ron van der Meyden, and Yoram Moses.
A program refinement framework supporting reasoning about knowledge
and time.
In Jerzy Tiuryn, editor, <em>Foundations of Software Science and
Computation Structures</em>, volume 1784 of <em>LNCS</em>, pages 114–129.
Springer-Verlag, March 2000.
[ <a href="kai-e-pubs_bib.html#EvdMM2000:FOSSACS">bib</a> |
<a href="kai-e-pubs_abstracts.html#EvdMM2000:FOSSACS">Abstract</a> ]
</dd>
<dt>
[<a name="EvdM99:wsproc">21</a>]
</dt>
<dd>
~ 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, <em>Proceedings of the FLoC'99 Workshop Complexity-Theoretic and
Recursion-Theoretic Methods in Databases and Artificial Intelligence</em>, pages
81–90, July 6 1999.
[ <a href="kai-e-pubs_bib.html#EvdM99:wsproc">bib</a> ]
</dd>
<dt>
[<a name="EvdMM98:TARK">22</a>]
</dt>
<dd>
~, Ron van der Meyden, and Yoram Moses.
Knowledge and the logic of local propositions.
In Itzhak Gilboa, editor, <em>Theoretical Aspects of Rationality and
Knowledge, Proceedings of the Seventh Conference (TARK 1998)</em>, pages 29–41.
Morgan Kaufmann, July 1998.
[ <a href="kai-e-pubs_bib.html#EvdMM98:TARK">bib</a> |
<a href="kai-e-pubs_abstracts.html#EvdMM98:TARK">Abstract</a> ]
</dd>
<dt>
[<a name="EdR:cup98">23</a>]
</dt>
<dd>
Willem-Paul de Roever and ~.
<em>Data Refinement: Model-Oriented Proof Methods and their
Comparison</em>.
Number 47 in Cambridge Tracts in Theoretical Computer Science.
Cambridge University Press, 1998.
Paperback re-issue 2009. Errata at
<a href="https://kai-e.github.io/pubs/dRE1998/errata.pdf">https://kai-e.github.io/pubs/dRE1998/errata.pdf</a>.
[ <a href="kai-e-pubs_bib.html#EdR:cup98">bib</a> ]
</dd>
<dt>
[<a name="E:PhD">24</a>]
</dt>
<dd>
~.
<em>Model-Oriented Data Refinement</em>.
PhD thesis, Institut für Informatik und Praktische Mathematik,
Christian-Albrechts-Universität zu Kiel, July 1997.
[ <a href="kai-e-pubs_bib.html#E:PhD">bib</a> |
<a href="kai-e-pubs_abstracts.html#E:PhD">Abstract</a> ]
</dd>
<dt>
[<a name="EdR:liberPV">25</a>]
</dt>
<dd>
~ and Willem-Paul de Roever.
New win[e/d] for old bags.
In John Tromp, editor, <em>A dynamic and quick intellect, Paul
Vitányi 25 years @ CWI</em>, pages 59–66. CWI, Amsterdam, November 1996.
[ <a href="kai-e-pubs_bib.html#EdR:liberPV">bib</a> ]
</dd>
<dt>
[<a name="EdR:mfcs96">26</a>]
</dt>
<dd>
~ and Willem-Paul de Roever.
Simulation of specification statements in Hoare logic.
In Wojciech Penczek and Andrzej Szalas, editors, <em>Mathematical
Foundations of Computer Science 1996, 21st International Symposium, MFCS
'96, Cracow, Poland, Proceedings</em>, volume 1113 of <em>LNCS</em>, pages
324–335. Springer-Verlag, September 1996.
[ <a href="kai-e-pubs_bib.html#EdR:mfcs96">bib</a> |
<a href="kai-e-pubs_abstracts.html#EdR:mfcs96">Abstract</a> ]
</dd>
<dt>
[<a name="EdR:facs95">27</a>]
</dt>
<dd>
~ and Willem-Paul de Roever.
Towards a practitioners' approach to Abadi and Lamport's method.
<em>Formal Aspects of Computing</em>, 7(5):550–575, 1995.
[ <a href="kai-e-pubs_bib.html#EdR:facs95">bib</a> |
<a href="kai-e-pubs_abstracts.html#EdR:facs95">Abstract</a> ]
</dd>
<dt>
[<a name="EdR:fme93">28</a>]
</dt>
<dd>
~ 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, <em>FME '93:
Industrial-Strength Formal Methods</em>, volume 670 of <em>LNCS</em>, pages
294–313. Springer-Verlag, April 1993.
[ <a href="kai-e-pubs_bib.html#EdR:fme93">bib</a> ]
</dd>
<dt>
[<a name="E:master93">29</a>]
</dt>
<dd>
~.
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.
[ <a href="kai-e-pubs_bib.html#E:master93">bib</a> |
<a href="kai-e-pubs_abstracts.html#E:master93">Abstract</a> ]
</dd>
</dl>