%% bibtexfile "mcrl.bib" %% created by Mark van der Zwaag @string{fac = "Formal Aspects of Computing"} @string{tcs = "Theoretical Computer Science"} @string{SV = "Springer-Verlag"} @string{UULGP = "Utrecht University, Logic Group Preprint Series"} @string{UvAPRG = "University of Amsterdam, Programming Research Group"} @string{LNCS = "LNCS"} %Lecture Notes in Computer Science @string{CWIA = "CWI, Amsterdam"} @TechReport{R9076, author = {Groote, J.F. and Ponse, A.}, title = {{T}he syntax and semantics of $\mu${CRL}}, institution = {CWI, Amsterdam}, number = {CS-R9076}, year = {1990} } @TechReport{R9138, author = {Groote, J.F. and Ponse, A.}, title = {{A} proof theory for $\mu${CRL}}, institution = {CWI, Amsterdam}, number = {CS-R9138}, year = {1991} } @inproceedings{gp94, author = {Groote, J.F. and Ponse, A.}, title = {{P}roof theory for $\mu${CRL}: a language for processes with data}, editor = {Andrews and others}, booktitle = {Proceedings of the International Workshop on Semantics of Specification Languages}, series = {Workshops in Computing Series}, pages = {231--250}, publisher = SV, year = 1994 } @inproceedings{gp95, author = {Groote, J.F. and Ponse, A.}, title = {The syntax and semantics of $\mu${CRL}}, editor = {Ponse, A. and C. Verhoef and Vlijmen, S.F.M. van}, booktitle = {Algebra of Communicating Processes '94}, series = {Workshops in Computing Series}, publisher = SV, pages = {26--62}, year = 1995 } @TechReport{PU:01, author = {Ponse, A. and Usenko, Y. S.}, title = {Equivalence of recursive specifications in process algebra}, institution = {CWI, Amsterdam}, year = 2001, number = {SEN-R0107} } %%%%%%%%%%%%%%%%%% Theory %%%%%%%%%%%%%%%%%%%%%%%%%%% @TechReport{GP:00, author = {Groote, J.F. and Pol, J. C. van de}, title = {State space reduction using partial tau-confluence}, institution = {CWI, Amsterdam}, year = 2000, number = {SEN-R0008} } @TechReport{GPU:00, author = {Groote, J.F. and Ponse, A. and Usenko, Y. S.}, title = {Linearization in parallel $p${CRL}}, institution = {CWI, Amsterdam}, year = 2000, number = {SEN-R0019} } @Article{GroVaa:92, author = {Groote, J.F. and F.W. Vaandrager}, title = {Structured operational semantics and bisimulation as a congruence}, journal = {Information and Computation}, year = 1992, volume = 100, number = 2, pages = {202--260} } @TechReport{gl98, author = {Groote, J.F. and Luttik, S.P.}, title = {Undecidability and completeness results for process algebras with alternative quantification over data}, institution = {CWI, Amsterdam}, year = 1998, number = {SEN-R9806}, note = {ftp://ftp.cwi.nl/pub/CWIreports/SEN/SEN-R9806.ps.Z} } @TechReport{gl98a, author = {Groote, J.F. and Luttik, S.P.}, title = {A complete axiomatisation of branching bisimulation for process algebras with alternative quantification over data}, institution = {CWI, Amsterdam}, year = 1998, number = {SEN-R9830}, note = {ftp://ftp.cwi.nl/pub/CWIreports/SEN/SEN-R9830.ps.Z} } @TechReport{l99, author = {Luttik, S.P.}, title = {Cylindric process algebras with conditionals give substitutionless $p${CRL}}, institution = {CWI, Amsterdam}, year = 1999, number = {SEN-R9912}, note = {ftp://ftp.cwi.nl/pub/CWIreports/SEN/SEN-R9912.ps.Z} } @TechReport{l99a, author = {Luttik, S.P.}, title = {Complete axiomatisations of weak-, delay- and $\eta$-bisimulation for process algebras with alternative quantification over data}, institution = {CWI, Amsterdam}, year = 1999, number = {SEN-R9914}, note = {ftp://ftp.cwi.nl/pub/CWIreports/SEN/SEN-R9914.ps.Z} } @TechReport{R9626, author = {Groote, J.F.}, title = {A Note on $n$ similar parallel processes}, number = {CS-R9626}, institution = {CWI, Amsterdam}, year = 1996, note = {ftp://ftp.cwi.nl/pub/CWIreports/AP/CS-R9626.ps.Z} } @article{Pon:96, author = {Ponse, A.}, title = {Computable processes and bisimulation equivalence}, journal = fac, volume = 8, year = 1996, pages = {648--678} } @Article{KorSel98a, author = {Korver, H.P. and Sellink, M.P.A.}, title = {A formal axiomatization for alphabet reasoning with parametrized processes}, journal = fac, year = 1998, volume = 10, pages = {30--42} } @TechReport{pre134, author = {Korver, H.P.}, title = {A formal axiomatization for alphabet reasoning with parametrized processes}, institution = UULGP, number = 134, year = 1995, note = {ftp://ftp.phil.uu.nl/pub/logic/PREPRINTS/preprint134.ps.Z} } @TechReport{P9409, author = {Groote, J.F. and Wamel, J.J. van}, title = {Algebraic data types and induction in $\mu${CRL}}, institution = UvAPRG, number = {P9409}, year = 1994 } @TechReport{P9511, author = {Bergstra, J.A. and Hillebrand, J.A. and Ponse, A.}, title = {Grid protocols based on synchronous communication: specification and correctness}, institution = UvAPRG, number = {P9511}, year = 1995, note = {http://ftp.wins.uva.nl/pub/programming-research/reports/1995/P9511.ps.Z} } @TechReport{P9410, author = {Wamel, J.J. van}, title = {Inductive proofs with sets, and some applications in process algebra}, institution = UvAPRG, number = {P9410}, year = 1994, note = {http://ftp.wins.uva.nl/pub/programming-research/reports/1994/P9410.ps.Z} } %%%%%%%%%%%%%%%%%%% Tools %%%%%%%%%%%%%%%%%%%%%%%%%%% @TechReport{L:01, author = {Langevelde, I. A. van}, title = {A compact file format for labeled transition systems}, institution = {CWI, Amsterdam}, year = 2001, number = {SEN-R0102} } @TechReport{vdP:01, author = {Pol, J. C. van de}, title = {A Prover for the mu{CRL} toolset with applications -- version 0.1}, institution = {CWI, Amsterdam}, year = 2001, number = {SEN-R0106} } @inproceedings{bp95, author = {Bosscher, D. and Ponse, A.}, title = {Translating a process algebra with symbolic data values to linear format}, editor = {Engberg, U.H. and Larsen, K.G. and Skou, A.}, booktitle = {Proceedings of the Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Aarhus 1995}, series = {BRICS Notes Series}, pages = {119--130}, publisher = {University of Aarhus}, year = 1995 } @TechReport{Kor:96, author = {H.P. Korver}, title = {Building a simulator in the $\mu${CRL} toolbox. {A} case study in modern software engineering}, institution = {CWI, Amsterdam}, year = 1996, number = {CS-R9632}, note = {ftp://ftp.cwi.nl/pub/CWIreports/AP/CS-R9632.ps.Z} } @TechReport{pre152, author = {Dams, D. and Groote, J.F.}, title = {Specification and implementation of components of a $\mu${CRL} toolbox}, institution = UULGP, number = 152, year = 1995, note = {ftp://ftp.phil.uu.nl/pub/logic/PREPRINTS/preprint152.ps.Z} } @TechReport{P9501, author = {Hillebrand, J.A. and Korver, H.P.}, title = {A well-formedness checker for $\mu${CRL}}, institution = UvAPRG, number = {P9501}, year = 1995, note = {http://ftp.wins.uva.nl/pub/programming-research/1995/P9501.ps.Z} } %%%%%%%%%%%%%% Verification Techniques %%%%%%%%%%%%%%%%%%%%%%%%%% @InCollection{GR:01, author = {Groote, J. F. and Reniers, M. A.}, title = {Algebraic Process Verification}, booktitle = {Handbook of Process Algebra}, publisher = {Elsevier}, year = 2001, editor = {Bergstra, J. A. and Ponse, A. and Smolka, S. A.}, chapter = 17 } @TechReport{GroSpr:95, author = {Groote, J.F. and Springintveld, J.}, title = {Focus points and convergent process operators. A proof strategy for protocol verification}, institution = UULGP, number = 142, year = 1995, note = {ftp://ftp.phil.uu.nl/pub/logic/PREPRINTS/preprint142.ps.Z} } @article{BezBolGro:97, author = {Bezem, M.A. and Bol, R.N. and Groote, J.F.}, title = {Formalizing process algebraic verifications in the Calculus of Constructions}, journal = fac, volume = 9, pages = {1--48}, year = 1997 } @inproceedings{BezGro:93b, author = {Bezem, M.A. and Groote, J.F.}, title = {Invariants in process algebra with data}, editor = {Jonsson, B. and Parrow, J.}, booktitle = {Proceedings Concur'94}, address = {Uppsala, Sweden}, series = LNCS, volume = 836, pages = {401--416}, publisher = SV, year = 1994 } @inproceedings{GroSel:95, author = {Groote, J.F. and Sellink, M.P.A}, title = {Confluence for process verification}, editor = {Smolka, S.A.}, booktitle = {Proceedings of {CONCUR'95}}, pages = {204--218}, series = LNCS, volume = 962, publisher = SV, year = 1995, note = {Extended abstract appeared as \cite{GroSel:96}} } @article{GroSel:96, author = {Groote, J.F. and Sellink, M.P.A}, title = {Confluence for process verification}, journal = {Theoretical Computer Science B (Logic, semantics and theory of programming)}, pages = {47--81}, volume = 170, number = {1--2}, year = 1996, note = {Also appeared as \cite{GroSel:95}, available as Technical Report 137, LGPS, Department of Philosophy, Utrecht University, 1995, ftp://ftp.phil.uu.nl/pub/logic/PREPRINTS/preprint154.ps.Z} } @incollection{GrovVl:95, author = {Groote, J.F. and Vlijmen, S.F.M. van}, title = {A modal logic for $\mu${CRL}}, booktitle = {Modal Logic and Process Algebra, a Bisimulation Perspective}, editor = {Ponse, A. and Rijke, M. de and Venema, Y.}, publisher = {CSLI Lecture Notes}, volume = 53, pages = {131--150}, address = {Stanford}, year = 1995 } @TechReport{BezGro:93, author = {Bezem, M.A. and Groote, J.F.}, title = {Proving a graph well founded using resolution. A case study in automated verification}, institution = UULGP, number = 113, year = 1993, note = {ftp://ftp.phil.uu.nl/pub/logic/PREPRINTS/preprint113.ps.Z} } @TechReport{KorSel:96, author = {Korver, H.P. and Sellink, M.P.A.}, title = {On automating process algebra proofs}, institution = UULGP, number = 154, year = 1996, note = {ftp://ftp.phil.uu.nl/pub/logic/PREPRINTS/preprint154.ps.Z} } @TechReport{KorSel:95, author = {Korver, H.P. and Sellink, M.P.A.}, title = {Formalising {LPO}s and invariants in {C}oq}, institution = UULGP, number = 147, year = 1995, note = {ftp://ftp.phil.uu.nl/pub/logic/PREPRINTS/preprint100.ps.Z} } @inproceedings{Sel:94, author = {Sellink, M.P.A}, title = {Verifying process algebra proofs in type theory}, editor = {Andrews et al}, booktitle = {Proceedings of the International Workshop on Semantics of Specification Languages}, series = {Workshops in Computing Series}, pages = {315--339}, publisher = SV, year = 1994 } %%%%%%%%%%%%% Applications %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @TechReport{U:99, author = {Usenko, Y. S.}, title = {A comparison of {S}pin and the mu{CRL} toolset on {HAV}i leader election protocol}, institution = {CWI, Amsterdam}, year = 1999, number = {SEN-R9917} } @Article{KorSel98b, author = {Korver, H.P. and Sellink, M.P.A.}, title = {Example verifications using alphabet axioms}, journal = fac, year = 1998, volume = 10, pages = {43--58} } @InProceedings{GrMP:98, author = {Groote, J.F. and Monin, F. and Pol, J.C. van de}, title = {Checking verifications of protocols and distributed systems by computer}, booktitle = {Proceedings of Concur'98}, pages = {629--655}, year = 1998, editor = {Sangiorgi, D. and Simone, R. de}, volume = 1466, series = LNCS, address = {Sophia Antipolis}, publisher = SV } @TechReport{Lut:97, author = {Luttik, S.P.}, title = {Description and formal specification of the link layer of {P}1394}, institution = {CWI, Amsterdam}, year = 1997, number = {SEN-R9706}, note = {ftp://ftp.cwi.nl/pub/CWIreports/SEN/SEN-R9706.ps.Z}, sectie = {applications} } @TechReport{BezPon94, author = {Bezem, M.A. and Ponse, A.}, title = {Two finite specifications of a queue}, institution = UvAPRG, number = {P9424}, year = 1994, note = {http://ftp.wins.uva.nl/pub/programming-research/1994/P9424.ps.Z}, sectie = {applications} } @TechReport{BezGro93, author = {Bezem, M.A. and Groote, J.F.}, title = {A formal verification of the alternating bit protocol in the calculus of constructions}, institution = UULGP, number = 88, year = 1993, note = {ftp://ftp.phil.uu.nl/pub/logic/PREPRINTS/preprint88.ps.Z}, sectie = {applications} } @InProceedings{GrovdP96, author = {Groote, J.F. and Pol, J.C. van de}, title = {A bounded retransmission protocol for large data packets. {A} case study in computer checked verification}, booktitle = {Proceedings of AMAST'96}, pages = {536--550}, year = 1996, editor = {Wirsing, M. and Nivat, M}, volume = 1101, series = LNCS, publisher = SV, note = {Also appeared as~\cite{GrovdP93}} } @TechReport{GrovdP93, author = {Groote, J.F. and Pol, J.C. van de}, title = {A bounded retransmission protocol for large data packets. {A} case study in computer checked verification}, institution = UULGP, number = 100, year = 1993, note = {ftp://ftp.phil.uu.nl/pub/logic/PREPRINTS/preprint100.ps.Z, Also appeared as~\cite{GrovdP96}}, sectie = {applications} } @TechReport{KorSpr93, author = {Korver, H.P. and Springintveld, J.}, title = {A computer-checked verification of {M}ilner's scheduler}, institution = UULGP, number = 101, year = 1993, note = {ftp://ftp.phil.uu.nl/pub/logic/PREPRINTS/preprint101.ps.Z, Also appeared as~\cite{KorSpr94}}, sectie = {applications} } @InProceedings{KorSpr94, author = {Korver, H.P. and Springintveld, J.}, title = {A computer-checked verification of {M}ilner's scheduler}, booktitle = {Proceedings of the International Symposium on Theoretical Aspects of Computer Software (TACS'94)}, pages = {161--178}, year = 1994, editor = {Hagiya, M. and Mitchell, J.C.}, volume = 789, series = LNCS, publisher = SV, note = {Also appeared as~\cite{KorSpr93}} } @TechReport{GriKor95, author = {Griffioen, D. and Korver, H.P.}, title = {The Bakery Protocol: a comparative case-study in formal verification}, institution = UULGP, number = 136, year = 1995, note = {ftp://ftp.phil.uu.nl/pub/logic/PREPRINTS/preprint136.ps.Z}, sectie = {applications} } @TechReport{GroSpr96, author = {Groote, J.F. and Springintveld, J.}, title = {Algebraic verification of a Distributed Summation Algorithm}, number = {CS-R9640}, institution = {CWI, Amsterdam}, year = 1996, note = {ftp://ftp.cwi.nl/pub/CWIreports/AP/CS-R9640.ps.Z, Also appeared as \cite{GroSpr96a}}, sectie = {applications} } @TechReport{GroMonSpr97, author = {Groote, J.F. and Monin, F. and Springintveld, J.}, title = {A computer checked algebraic verification of a distributed summing protocol}, number = {CS 97/14}, institution = {Department of Mathematics and Computer Science, Eindhoven University of Technology}, year = 1997, sectie = {applications} } @TechReport{GroSpr96a, author = {Groote, J.F. and Springintveld, J.}, title = {Algebraic verification of a Distributed Summation Algorithm}, number = {CSI-R9627}, institution = {Department of Mathematics and Computer Science, University of Nijmegen}, year = 1996, note = {Also appeared as \cite{GroSpr96}}, sectie = {applications} } @article{BezGro94, author = {Bezem, M.A. and Groote, J.F.}, title = {A correctness proof of a one bit sliding window protocol in $\mu${CRL}}, journal = {The Computer Journal}, number = 4, volume = 37, pages = {289--307}, year = 1994, sectie = {applications} } @article{GroKoovVl95, author = {Groote, J.F. and Koorn, J.W.C. and Vlijmen, S.F.M. van}, title = {Formele analyse van het veiligheidssysteem op het station van {H}oorn-{K}ersenboogerd}, journal = {Informatie, {\rm Jaargang 36}}, volume = 6, pages = {397--404}, year = 1995, sectie = {applications} } @inproceedings{GroKoovVl95a, author = {Groote, J.F. and Koorn, J.W.C. and Vlijmen, S.F.M. van}, title = {The safety guaranteeing system at station {H}oorn-{K}ersenboogerd (Extended abstract)}, booktitle = {Proceedings 10th Annual Conference on Computer Assurance (COMPASS'95)}, pages = {57--68}, address = {Gaithersburg, {M}aryland}, year = 1995, sectie = {applications} } @inproceedings{GroKor94, author = {Groote, J.F. and Korver, H.P.}, title = {{C}orrectness proof of the bakery protocol in $\mu${CRL}}, editor = {Ponse, A. and Verhoef, C. and Vlijmen, S.F.M. van}, booktitle = {Algebra of Communicating Processes '94}, series = {Workshops in Computing Series}, publisher = SV, pages = {63--86}, year = 1995, sectie = {applications} } @article{FreGroKor95, author = {Fredlund, L.-{\AA}. and Groote, J.F. and Korver, H.P.}, title = {Formal verification of a leader election protocol in process algebra}, journal = tcs, volume = 177, pages = {459--486}, year = 1997, sectie = {applications} } @article{SvdZ98, author = {Shankland, C. and Zwaag, M.B. van der}, title = {The tree identify protocol of {IEEE} 1394 in $\mu${CRL}}, journal = fac, volume = 10, pages = {509--531}, year = 1998, note = {Also available as Technical report SEN-R9831, CWI, Amsterdam, ftp://ftp.cwi.nl/pub/CWIreports/SEN/SEN-R9831.ps.Z} } %%%%%%%%%%%%% Timed mCRL %%%%%%%%%%%%%%%%%%%% @TechReport{R9709, author = {Groote, J.F.}, title = {The syntax and semantics of timed $\mu${CRL}}, institution = {CWI, Amsterdam}, number = {SEN-R9709}, year = 1997, note = {ftp://ftp.cwi.nl/pub/CWIreports/SEN/SEN-R9709} } @TechReport{GrovWa:98, author = {Groote, J.F. and Wamel, J.J. van}, title = {Basic theorems for parallel processes in timed $\mu${CRL}}, institution = {CWI, Amsterdam}, year = 1998, number = {SEN-R9808}, note = {ftp://ftp.cwi.nl/pub/CWIreports/SEN/SEN-R9808}, abstract = {ftp://ftp.cwi.nl/pub/CWIreports/abs/SEN-R9808.html} } @Article{GrovWa:01, author = {Groote, J.F. and Wamel, J.J. van}, title = {Analysis of three hybrid systems in timed $\mu${CRL}}, journal = {Science of Computer Programming}, year = 2001, volume = 39, pages = {215--247}, note = {An earlier version is available as Technical Report SEN-R9815, CWI, Amsterdam, ftp://ftp.cwi.nl/pub/CWIreports/SEN/SEN-R9815.ps.Z} } @TechReport{Zwa:00, author = {Zwaag, M. B. van der}, title = {Time-stamped actions in $p${CRL} algebras}, institution = {CWI, Amsterdam}, year = 2000, number = {SEN-R0002}, note = {ftp://ftp.cwi.nl/pub/CWIreports/SEN/SEN-R0002.ps.Z} } @TechReport{GRWZ:00, author = {Groote, J.F. and Reniers, M. A. and Wamel, J.J. van and Zwaag, M. B. van der}, title = {Completeness of timed $\mu${CRL}}, institution = {CWI, Amsterdam}, year = 2000, number = {SEN-R0034}, note = {ftp://ftp.cwi.nl/pub/CWIreports/SEN/SEN-R0034.ps.Z} } @TechReport{Zwa:00a, author = {Zwaag, M. B. van der}, title = {The cones and foci proof technique for timed transition systems}, institution = {CWI, Amsterdam}, year = 2000, note = {ftp://ftp.cwi.nl/pub/CWIreports/SEN/SEN-R0038.ps.Z, accepted for publication in \emph{Information Processing Letters}} }