@STRING{lncs = "Lecture Notes in Computer Science" } @STRING{softtech= "Lehrstuhl f{\"ur} Software-Technologie, Institut f{\"u}r Informatik und Praktische Mathematik, Christian-Albrechts-Universit{\"a}t zu Kiel" } @STRING{sv = "Springer-Verlag" } @InProceedings{CKdR92, author = "Antonio Cau and Ruurd Kuiper and Willem-Paul de Roever", title = "Formalizing {D}ijkstra's development strategy within {S}tark's formalism", editor = "Cliff B. Jones and Roger C. Shaw and Tim Denvir", booktitle = "Proc. 5th. BCS-FACS Refinement Workshop", year = 1992 } @InProceedings{CdR93a, author = "Antonio Cau and Willem-Paul de Roever", title = "Using Relative Refinement for Fault Tolerance", booktitle = "Proceedings of FME'93 symposium: Industrial Strength Formal Method", year = 1993 } @InProceedings{CdR93b, author = "Antonio Cau and Willem-Paul de Roever", title = "Specifying Fault Tolerance within {S}tark's Formalism", booktitle = "Proc.\ of the Twenty-Third International Symposium on Fault-Tolerant Computing", year = 1993 } @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-Verlag", 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}", editor = "Jim C.P. Woodcock and Peter Gorm Larsen", volume = 670, series = "{LNCS}", pages = "294--313", booktitle = "{FME} '93: Industrial-Strength Formal Methods", year = 1993, publisher = "Springer-Verlag", month = "April" } @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-Verlag", month = sep, pages = "324--335" } @Book{dRE98, author = {Willem-Paul de Roever and Kai Engelhardt}, title = {Data Refinement: Model-Oriented Proof Methods and their Comparison}, publisher = {Cambridge University Press}, year = 1998, number = 47, series = {Cambridge Tracts in Theoretical Computer Science}, address = {Cambridge, UK}, month = nov, isbn = {0 521 64170 5} } @Article{FHLdR79, author = "Nissim Francez and C.A.R Hoare and D. Lehmann and Willem-Paul de Roever", title = "Semantics of Nondeterminism, Concurrency, and Communication", journal = "JCSS", year = 1979 } @Article{GFMdR83, author = "O. Gr{\"u}mberg and N. Francez and J. Makowski and Willem-Paul de Roever", title = "A proof rule for fair termination", journal = "Information and Control", year = 1983, volume = 66, number = "1/2" } @Article{HRdR, author = "Jozef Hooman and S. Ramesh and Willem-Paul de Roever", title = "A compositional axiomatization of {Statecharts}", journal = "Theoretical Computer Science", year = 1992, volume = 101, pages = "289--335" } @article{HuideR91, author = {Cees Huizing and Willem-Paul de Roever}, journal = {Information {P}rocessing {L}etters 37}, pages = {205-213}, title = {Introduction to design choices in the semantics of {S}tatecharts}, year = {1991} } @InBook{KdR82, author = "Ruurd Kuiper and Willem-Paul de Roever", title = "Formal Description of Programming Concepts II", chapter = "Fairness for CSP in a temporal logic framework", publisher = " North-Holland", year = 1982 } @InProceedings{KdRV83, author = "Ron Koymans and Willem-Paul de Roever and Jan Vytopil", title = "A formal system for a telecommunication language: a case study in proofs about real-time programming and asynchronous message passing", booktitle = "Proc. of 2nd Conference on Principles of Distributed Computing", year = 1983 } @InProceedings{PHPdR94a, author = {Carsta Petersohn and Cees Huizing and Jan Peleska and Willem-Paul de Roever}, title = {Formal Semantics for {Ward \& Mellor`s TRANSFORMATION SCHEMAS}}, booktitle = {6th Refinement Workshop}, editor = {D. Till}, organization = {BCS-FACS}, pages = {14--41}, publisher = {Springer Verlag}, series = {Workshops in Computing}, year = {1994} } @InProceedings{PHPdR94b, author = "Carsta Petersohn and Cees Huizing and Jan Peleska and Willem-Paul de Roever", title = {Formal Semantics for {Ward \& Mellor`s TRANSFORMATION SCHEMAS} -- An Overview}, booktitle = {Proceedings of the Workshop on Formal Methods for Information System Dynamics of the Conference {CAiSE94}}, editor = {E. Dubois and P. Hartel and G. Saake}, pages = {102--113}, publisher = {University of Twente}, series = {Mamoranda Informatica 94-33}, year = {1994} } @InProceedings{PHPdR94c, author = {Carsta Petersohn and Cees Huizing and Jan Peleska and Willem-Paul de Roever}, title = {Formal Semantics for {Ward \& Mellor`s TRANSFORMATION SCHEMAS} and the {Specification of Fault-Tolerant Systems}}, booktitle = {Dependable Computing -- EDCC-1 (First European Dependable Computing Conference)}, editor = {K. Echtle and D. Hammer and D. Powell}, pages = {59--76}, series = {LNCS}, volume = {852}, year = {1994} } @TechReport{PPHdR94a, author = "Carsta Petersohn and Jan Peleska and Cees Huizing and Willem-Paul de Roever", title = "Formal Semantics for {W}ard \& {M}ellor's {TRANSFORMATION SCHEMAS} and its Application to Fault-Tolerant Systems", institution = "Christian-Albrechts-Universit{\"a}t Kiel", year = 1994, number = 9420 } @InCollection{PPHdeR94b, author = "Carsta Petersohn and Jan Peleska and Cees Huizing and Willem-Paul de Roever", title = "Formal Semantics for Ward \& Mellor's TRANSFORMATION SCHEMAS and its Application to Fault-Tolerant Systems", year = 1994, series = "Dagstuhl-Seminar ``Synchrone Sprachen''" } @InProceedings{PdR82, author = "Amir Pnueli and Willem-Paul de Roever", title = "Rendez-Vous with ADA - a Proof Theoretic View", booktitle = "Proc.\ of {ADA-TEC} '82 Conference on {ADA}", year = 1982 } @Article{RdRS, author = "S. Ramesh and Willem-Paul de Roever and Frank Stomp", title = "A Compositional Axiomatization of {Statecharts}", journal = "Theoretical Computer Science" } @Article{SdR94, author = "Frank Stomp and Willem-Paul de Roever", title = "A Principle for Sequential Reasoning about Distributed Algorithms", journal = "Formal Aspects of Computing", year = 1994, volume = 6, number = 6, pages = "716--737" } @TechReport{XdRH95, author = "Qiwen Xu and Willem-Paul de Roever and Jifeng He", title = "Rely-Guarantee Methods for Verifying Shared Variable Concurrent Programs", year = 1995, } @InProceedings{ZHL+96, author = "Job Zwiers and Ulrich Hannemann and Yassine Lakhnech and Willem-Paul de Roever and Frank Stomp", title = "Modular Completeness: Integrating the Reuse of Specified Software in Top-Down Program Development", booktitle = "Formal Methods Europe 96", year = 1996, series = "LNCS", volume = 1051, publisher = "Springer-Verlag", } @InProceedings{ZHLdR95, author = "Job Zwiers and Ulrich Hannemann and Yassine Lakhnech and Willem-Paul de Roever", title = "Synthesizing Different Development Paradigms: Combining Top-Down with Bottom-Up Reasoning About Distributed Systems", booktitle = "{FST \& TCS Bangalore}", year = 1995, series = "LNCS", publisher = "Springer-Verlag", volume = 1026 } @InProceedings{ZHLdRS95, author = "Job Zwiers and Willem-Paul de Roever and Ulrich Hannemann and Yassine Lakhnech and Frank Stomp", title = "Modular Completeness", booktitle = "{FST \& TCS Bangalore}", year = 1995, series = "LNCS", publisher = "Springer-Verlag", volume = 1026 } @InProceedings{dBdRT95, author = {Frank de Boer and Willem-Paul de Roever and Haykal Tej}, title = {Compositionality in real-time shared variable concurrency, (preliminary version)}, booktitle = {Proc.\ of the '95 Nordic Seminar, Uppsala} } @InProceedings{dR85, author = "Willem-Paul de Roever", title = "The Quest for Compositionality---a Survey of Assertion-Based Proof Systems for Concurrent Programs, Part I: Concurrency Based on Shared Variables", booktitle = "Proc.\ of the {IFIP} Working Conference ``The role of abstract models in computer science''", year = 1985, publisher = "North-Holland" } @InProceedings{dRCZ93, author = "Willem-Paul de Roever and Jos Coenen and Job Zwiers", title = "A note on compositional refinement", editor = "Cliff B. Jones and Tim Denvir and Roger C. Shaw", booktitle = "Proc.\ 5th Refinement Workshop", year = 1993, publisher = "Workshops in Computing, Springer-Verlag" } @InProceedings{dRZ89, author = "Willem-Paul de Roever and J. Zwiers", title = "Predicates are predicate transformers : towards a unified theory of concurrency", booktitle = "Proc. of 8th Conference on Principles of Distributed Computing", year = 1989 } @Book{dRdBHHLPZ01, author = {Willem-Paul de Roever and Frank de Boer and Ulrich Hannemann and Jozef Hooman and Yassine Lakhnech and Mannes Poel and Job Zwiers}, title = {Concurrency Verification: Introduction to Compositional and Noncompositional Methods}, publisher = {Cambridge University Press}, year = 2001, number = 54, series = {Cambridge Tracts in Theoretical Computer Science}, address = {Cambridge, UK}, month = nov, isbn = {0-521-80608-9} } @InProceedings{vEdRZ85, author = "Peter van Emde Boas and Willem-Paul de Roever and Job Zwiers", title = "Compositionality and Concurrent Networks: Soundness and Completeness of a Proof System", series = "LNCS", volume = 194, booktitle = "Proc.\ of 12th colloquium on Automata, Languages and Programming", year = 1985 } @TechReport{ abraham.deboer.deroever.steffen:hoarelogic-rep, author = {Erika {\'A}brah{\'a}m and Frank S. de Boer and Willem-Paul de Roever and Martin Steffen}, title = {A {H}oare Logic for Monitors in {J}ava}, institution = softtech, year = 2003, type = "Techical report", number = "TR-ST-03-1", month = apr, url = "http://www.informatik.uni-kiel.de/inf/deRoever/techreports/02/tr-st-03-1.pdf" , abstract = "Besides the features of a class-based object-oriented language, \textsl{Java} integrates concurrency via its thread-classes, allowing for a \emph{multithreaded} flow of control. The concurrency model includes \emph{shared-variable} concurrency via instance variables, \emph{coordination} via reentrant synchronization monitors, \emph{synchronous message passing,} and dynamic \emph{thread creation.} To reason about safety-properties of multithreaded programs, we introduce in this paper a tool-supported \emph{assertional proof method} for \textsl{Java}$_\mathit{MT}$ (``\emph{Multi-Threaded Java}''), a small concurrent sublanguage of \textsl{Java}, covering the mentioned concurrency issues as well as the object-based core of \textsl{Java}, i.e., object creation, side effects, and aliasing, but leaving aside inheritance and subtyping. We show soundness and relative completeness of the proof method." } @InProceedings{ abraham.deboer.deroever.steffen:inductive, author = {Erika {\'A}brah{\'a}m and Frank S. de Boer and Willem-Paul de Roever and Martin Steffen}, title = {Inductive Proof-Outlines for Monitors in {J}ava}, crossref = "lncs-fmoods03", note = "To appear. A longer version appeared as Software Technologie technical report TR-ST-03-1, April 2003" } @InProceedings{ abrahammumm.deboer.deroever.steffen:compositionalsemantics, author = {Erika {\'A}brah{\'a}m and Frank S. de Boer and Willem-Paul de Roever and Martin Steffen}, title = {A Compositional Operational Semantics for {Java$_{{\it MT}}$}}, crossref = "lncs2772", note = "To appear. A preliminary version appeared as Technical Report TR-ST-02-2, May 2002", abstract = "Besides the features of a class-based object-oriented language, \textsl{Java} integrates concurrency via its thread-classes, allowing for a \emph{multithreaded} flow of control. The concurrency model includes \emph{shared-variable} concurrency via instance variables, \emph{coordination} via reentrant synchronization monitors, \emph{synchronous message passing,} and dynamic \emph{thread creation.} This report contains a compositional version of the operational semantics of {\textsl{Java}$_{\it MT}$}." } @TechReport{ abrahammumm.deboer.deroever.steffen:compositionalsemantics-rep, author = {Erika {\'A}brah{\'a}m-Mumm and Frank S. de Boer and Willem-Paul de Roever and Martin Steffen}, title = {A Compositional Operational Semantics for {Java$_{{\it MT}}$}}, institution = softtech, year = 2002, type = {Technical Report}, number = {TR-ST-02-2}, month = may, url = "http://www.informatik.uni-kiel.de/inf/deRoever/techreports/02/tr-st-02-2.ps.gz" , abstract = "Besides the features of a class-based object-oriented language, \textsl{Java} integrates concurrency via its thread-classes, allowing for a \emph{multithreaded} flow of control. The concurrency model includes \emph{shared-variable} concurrency via instance variables, \emph{coordination} via reentrant synchronization monitors, \emph{synchronous message passing,} and dynamic \emph{thread creation.} This report contains a compositional version of the operational semantics of {\textsl{Java}$_{\it MT}$}." } @TechReport{ abrahammumm.deboer.deroever.steffen:javamonitors-rep, author = {Erika {\'A}brah{\'a}m-Mumm and Frank S. de Boer and Willem-Paul de Roever and Martin Steffen}, title = {Verification for {J}ava's Monitor Concept: {S}oundness and Completeness}, institution = softtech, year = 2002, type = {Technical Report}, number = {TR-ST-02-3}, note = "to appear" } @InProceedings{ abrahammumm.deboer.deroever.steffen:multithreading, author = {Erika {\'A}brah{\'a}m-Mumm and Frank S. de Boer and Willem-Paul de Roever and Martin Steffen}, title = {Verification for {J}ava's Reentrant Multithreading Concept}, crossref = {lncs2303}, pages = {4--20}, note = "A longer version, including the proofs for soundness and completeness, appeared as Technical Report TR-ST-02-1, March 2002" } @TechReport{ abrahammumm.deboer.deroever.steffen:multithreading-rep, author = {Erika {\'A}brah{\'a}m-Mumm and Frank S. de Boer and Willem-Paul de Roever and Martin Steffen}, title = {Verification for {J}ava's Reentrant Multithreading Concept: {S}oundness and Completeness}, institution = softtech, year = 2002, type = {Technical Report}, number = {TR-ST-02-1} } @InProceedings{ abrahammumm.deboer.deroever.steffen:toolsupported, author = {Erika {\'A}brah{\'a}m-Mumm and Frank S. de Boer and Willem-Paul de Roever and Martin Steffen}, title = "A Tool-Supported Proof System for Monitors in {J}ava", booktitle = "Proceedings of the FMCO 2002", year = 2002, note = "To appear" } @Proceedings{ lncs2303, key = "FoSSaCS2002", title = {Proceedings of the 5th International Conference on Foundations of Software Science and Computation Structures ({FoSSaCS} 2002), Held as Part of the Joint European Conferences on Theory and Practice of Software ({ETAPS} 2002), (Grenoble, France, April 8-12, 2002)}, booktitle = {Proceedings of {FoSSaCS} 2002}, year = 2002, editor = "Mogens Nielsen and Uffe H. Engberg", volume = 2303, series = lncs, month = apr, publisher = sv, crossrefonly = 1 } @Proceedings{ lncs2772, title = "Proceedings of the International Symposium on Verification (Theory and Practice) Celebrating Zohar Manna's 64th Birthday, Taormina, Sicily, June 29--July 4, 2003", year = 2003, booktitle = "International Symposium on Verification (Theory and Practice)", editor = "Nachum Derschowitz", volume = 2772, series = lncs, publisher = sv, annote = "Check the data" } @Proceedings{ lncs-fmoods03, title = "Proceedings of the 6th IFIP International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS '03), Paris", booktitle = "FMOODS '03", year = 2003, editor = "Uwe Nestmann and Perdita Stevens", series = lncs, month = nov, publisher = sv }