@PhdThesis{E:PhD, author = {Kai Engelhardt}, title = {Model-Oriented Data Refinement}, school = ifi, pages = 280, year = 1997, month = jul, abstract = {The goal of this thesis is to provide a comprehensive and systematic introduction to the important and highly applicable method of data refinement and proving simulation. We concentrate in the first part on the general principles needed to prove data refinement correct, and begin with an explanation of the fundamental notions, showing that data refinement proofs reduce to proving simulation. The topics of Hoare Logic and the Refinement Calculus are then introduced and a general theory of simulations is developed and related to them. Accessibility and comprehension are emphasised in order to guide newcomers to the area. The second part of this thesis contains a detailed survey of important methods in this area, such as VDM, and the methods due to Abadi \& Lamport, Hehner, Lynch and Reynolds, and Back's refinement calculus. All these methods are carefully analysed, and shown to be either incomplete, with counterexamples to their application, or to be always applicable whenever data refinement holds. This is shown by proving, for the first time, that all of them can be described and analysed in terms of two simple notions: forward and backward simulation.} } @MastersThesis{E:master93, author = {Kai Engelhardt}, title = {{Verallgemeinerungen der Methode von Abadi und Lamport um ein von A. Pnueli gestelltes Problem zu l\"{o}sen}}, school = ifi, year = 1993, month = jan, annote = {German title but English text} } @Book{EdR:cup98, author = {Willem-Paul de Roever and Kai Engelhardt}, title = {Data Refinement: Model-Oriented Proof Methods and their Comparison}, publisher = cup, pages = 430, year = 1998, number = 47, series = cttcs, annote = {With the assistance of Jos Coenen, Karl-Heinz Buth, Paul Gardiner, Yassine Lakhnech, and Frank Stomp}, annote = {$\pounds$45\,/\,US\$69.95\,/\,AU\$125} } @Article{EdR:facs95, author = {Kai Engelhardt and Willem-Paul de Roever}, title = {Towards a Practitioners' Approach to {Abadi} and {Lamport's} Method}, journal = {Formal Aspects of Computing}, publisher = springer, year = 1995, volume = 7, number = 5, pages = {550--575} } @InProceedings{EdR:fme93, author = {Kai Engelhardt and Willem-Paul de Roever}, title = {Generalizing {Abadi} \& {Lamport's} Method to Solve a Problem Posed by {A. Pnueli}}, booktitle = {{FME} '93: Industrial-Strength Formal Methods}, editor = {Jim C.P. Woodcock and Peter Gorm Larsen}, volume = 670, series = lncs, year = 1993, publisher = springer, month = apr, pages = {294--313}, annote = {Contains an error} } @InCollection{EdR:liberPV, author = {Kai Engelhardt and Willem-Paul de Roever}, title = {New Win\begin{tabular}{@{}l@{}}e\\\hline d\end{tabular} for Old Bags}, booktitle = {A dynamic and quick intellect, {Paul Vit\'{a}nyi 25 years @ CWI}}, publisher = {CWI}, year = 1996, editor = {John Tromp}, address = {Amsterdam}, month = nov, pages = {59--66}, annote = {A more descriptive title would be ``A pure, sound, and complete (in the sense of Cook) Hoare logic for a language with specification statements and recursion'', which is definitely too long} } @InProceedings{EdR:mfcs96, author = {Kai Engelhardt and Willem-Paul de Roever}, title = {Simulation of Specification Statements in {Hoare} Logic}, booktitle = {Mathematical Foundations of Computer Science 1996, 21st International Symposium, {MFCS '96}, Cracow, Poland, Proceedings}, editor = {Wojciech Penczek and Andrzej Sza{\l}as}, volume = 1113, series = lncs, year = 1996, publisher = springer, month = sep, pages = {324--335} } @InProceedings{EvdM99:wsproc, author = {Kai Engelhardt and Ron van der Meyden}, title = {Modal Logics with a Hierarchy of Local Propositional Quantifiers (Extended Abstract)}, booktitle = {Proceedings of the {FLoC'99} Workshop Complexity-Theoretic and Recursion-Theoretic Methods in Databases and Artificial Intelligence}, pages = {81--90}, year = 1999, editor = {Thomas Eiter and Georg Gottlob and Victor Marek and Jeffrey Remmel}, month = jul # { 6} } @InProceedings{EvdMS2002:AiML, author = {Kai Engelhardt and Ron van der Meyden and Kaile Su}, title = {Modal Logics with a Linear Hierarchy of Local Propositional Quantifiers}, OPTcrossref = {}, OPTkey = {}, booktitle = {Advances in Modal Logic 2002}, OPTpages = {}, year = 2002, editor = {Nobu-Yuki Suzuki and Frank Wolter}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, OPTaddress = {}, OPTmonth = {}, OPTorganization ={}, OPTpublisher = {}, OPTnote = {}, OPTannote = {} } @InProceedings{E2002:RefWS, author = {Kai Engelhardt}, title = {Towards a Refinement Theory that Supports Reasoning about Knowledge and Time for Multiple Agents (Work in Progress)}, OPTcrossref = {}, OPTkey = {}, booktitle = {Proceedings of {REFINE} 2002 --- A Refinement Workshop}, OPTpages = {}, year = 2002, editor = {John Derrick and Eerke Boiten}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, OPTaddress = {}, OPTmonth = {}, OPTorganization ={}, OPTpublisher = {}, OPTnote = {}, OPTannote = {} } @Unpublished{EvdM:notesonfine, author = {Kai Engelhardt and Ron van der Meyden}, title = {S5 with propositional quantification: Decidability, Complexity, and Axiomatization}, note = {unpublished}, month = feb, year = 2001 } @InProceedings{EvdMM2000:FOSSACS, author = {Kai Engelhardt and Ron van der Meyden and Yoram Moses}, title = {A Program Refinement Framework Supporting Reasoning about Knowledge and Time}, booktitle = {Foundations of Software Science and Computation Structures}, pages = {114--129}, year = 2000, editor = {Jerzy Tiuryn}, volume = 1784, series = lncs, month = mar, publisher = springer } @InProceedings{EvdMM98:TARK, author = {Kai Engelhardt and Ron van der Meyden and Yoram Moses}, title = {Knowledge and the Logic of Local Propositions}, booktitle = {Theoretical Aspects of Rationality and Knowledge, Proceedings of the Seventh Conference (TARK 1998)}, pages = {29--41}, year = 1998, month = jul, editor = {Itzhak Gilboa}, publisher = {Morgan Kaufmann} } @InProceedings{EvdMM2001:LPAR, author = {Kai Engelhardt and Ron van der Meyden and Yoram Moses}, title = {A Refinement Theory that Supports Reasoning about Knowledge and Time for Synchronous Agents}, booktitle = {Proceedings {LPAR} 2001}, pages = {125--141}, year = 2001, editor = {Robert Nieuwenhuis and Andrei Voronkov}, volume = 2250, series = lnai, month = dec, publisher = springer } @InProceedings{EM2005a, author = {Kai Engelhardt and Yoram Moses}, title = {Causing Communication Closure: Safe Program Composition with Non-{FIFO} Channels}, booktitle = {{DISC 2005} 19$^\mathrm{th}$ International Symposium on Distributed Computing}, pages = {229--243}, year = 2005, editor = {Pierre Fraigniaud}, volume = 3724, series = lncs, month = sep # { 26--28}, publisher = springer, url = {http://www.cse.unsw.edu.au/~kaie/Papers/Ebib/Ebib.html#EM2005a} } @InProceedings{EM2005b, author = {Kai Engelhardt and Yoram Moses}, title = {Safe Composition of Distributed Programs Communicating over Order-Preserving Imperfect Channels}, booktitle = {7$^\mathrm{th}$ International Workshop on Distributed Computing {IWDC 2005}}, OPTpages = {??--??}, year = 2005, editor = {Ajay Kshemkalyani and Ajit Pal}, OPTvolume = {????}, series = lncs, month = dec # { 27--30}, publisher = springer, url = {http://www.cse.unsw.edu.au/~kaie/Papers/Ebib/Ebib.html#EM2005b} } @InProceedings{EM2005c, author = {Kai Engelhardt and Yoram Moses}, title = {Single-Bit Messages are Insufficient in the Presence of Duplication}, booktitle = {7$^\mathrm{th}$ International Workshop on Distributed Computing {IWDC 2005}}, OPTpages = {??--??}, year = 2005, editor = {Ajay Kshemkalyani and Ajit Pal}, OPTvolume = {????}, series = lncs, month = dec # { 27--30}, publisher = springer, url = {http://www.cse.unsw.edu.au/~kaie/Papers/Ebib/Ebib.html#EM2005c} } @Unpublished{E2005coin1, author = {Kai Engelhardt}, title = {How to (Specify to) Flip a Coin}, note = {Unpulished note; see~\url{ftp://ftp.cse.unsw.edu.au/pub/users/kaie/E2005coin1.pdf}} }