µCRL References

1. µCRL
2. Theory
3. Verification Techniques
4. Tools
5. Applications
6. Timed µCRL

1. µCRL
   • J.F. Groote and A. Ponse. The syntax and semantics of µCRL. In A. Ponse, C. Verhoef and S.F.M. van Vlijmen, editors, Algebra of Communicating Processes '94, Workshops in Computing Series, Springer-Verlag, pp. 26-62, 1995.
     Also appeared as: Technical Report CS-R9076, CWI, Amsterdam, 1990.
   • J.F. Groote and A. Ponse. Proof theory for µCRL: a language for processes with data. In Andrews et al., editors, Proceedings of the International Workshop on Semantics of Specification Languages, Workshops in Computing Series, pages 231-250, Springer-Verlag, 1994.
     Also appeared as: Technical Report CS-R9138, CWI, Amsterdam, 1991.
   • J.F. Groote. The syntax and semantics of timed µCRL. Technical Report SEN-R9709, CWI, Amsterdam, 1997. (Abstract)

Top of page

2. Theory
   • J.A. Bergstra, J.A. Hillebrand, and A. Ponse. Grid protocols based on synchronous communication: specification and correctness. Technical Report P9511, University of Amsterdam, Programming Research Group, 1995. (Abstract)
   • J.F. Groote. A note on n similar parallel processes. Technical Report CS-R9626, CWI, Amsterdam, 1996.
   • J.F. Groote and S.P. Luttik. Undecidability and completeness results for process algebras with alternative quantification over data. Technical Report SEN-R9806, CWI, Amsterdam, 1998. ( Abstract) (Summary in postscript)
   • J.F. Groote and S.P. Luttik. A complete axiomatisation of branching bisimulation for process algebras with alternative quantification over data. Technical Report SEN-R9806, CWI, Amsterdam, 1998. (Abstract)
   • J.F. Groote and J.C. van de Pol. State space reduction using partial tau-confluence. Technical Report SEN-R0008, CWI, Amsterdam, 2000. ( Abstract)
   • J.F. Groote, A. Ponse and Y.S. Usenko. Linearization in parallel pCRL. Technical Report SEN-R0019, CWI, Amsterdam, 2000. ( Abstract)
   • J.F. Groote and F.W. Vaandrager. Structured operational semantics and bisimulation as a congruence. Information and Computation, 100(2):202-260, 1992.
   • J.F. Groote and J.J. van Wamel. Algebraic data types and induction in µCRL. Technical Report P9409, University of Amsterdam, Programming Research Group, 1994. (Abstract)
   • H.P. Korver and A. Sellink. A formal axiomatization for alphabet reasoning with parameterized processes. Formal Aspects of Computing, 10:30-42, 1998.
     Earlier version: H.P. Korver. A formal axiomatization for alphabet reasoning with parameterized processes. Technical Report 134, Logic Group Preprint Series, Utrecht University, 1995.
   • S.P. Luttik. Cylindric process algebras with conditionals give substitutionless pCRL. Technical Report SEN-R9912, CWI, Amsterdam, 1999. (Abstract)
   • S.P. Luttik. Complete axiomatisations of weak-, delay- and $\eta$-bisimulation for process algebras with alternative quantification over data. Technical Report SEN-R9914, CWI, Amsterdam, 1999. (Abstract)
   • A. Ponse. Computable processes and bisimulation equivalence. Formal Aspects of Computing, 8:648-678, 1996.
   • A. Ponse and Y.S. Usenko. Equivalence of recursive specifications in process algebra. Technical Report SEN-R0107, CWI, Amsterdam, 2001. ( Abstract)
   • J.J. van Wamel. Inductive proofs with sets, and some applications in process algebra. Technical Report P9410, University of Amsterdam, Programming Research Group, 1994. (Abstract)

Top of page

3. Verification Techniques
   • M.A. Bezem, R.N. Bol and J.F. Groote. Formalizing process algebraic verifications in the Calculus of Constructions. Formal Aspects of Computing 9:1-48, 1997.
   • M.A. Bezem and J.F. Groote. Invariants in process algebra with data. In B. Jonsson and J. Parrow, editors, Proceedings CONCUR'94, Uppsala, Sweden, LNCS 836, pages 401-416, Springer-Verlag, 1994.
   • M.A. Bezem and J.F. Groote. Proving a graph well founded using resolution. A case study in automated verification. Technical Report 113, Logic Group Preprint Series, Utrecht University, 1994.
   • J.F. Groote and M.A. Reniers. Algebraic Process Verification. In J.A. Bergstra, A. Ponse and S.A. Smolka, editors, Handbook of Process Algebra, chapter 17, Elsevier, 2001.
   • J.F. Groote and M.P.A. Sellink. Confluence for process verification. Theoretical Computer Science B (Logic, semantics and theory of programming), 170(1-2):47-81, 1996.
     Extended abstract in S.A. Smolka, editor, proceedings of CONCUR'95, pp. 204-218, LNCS 962, Springer-Verlag, 1995. Available as Technical Report 137, Logic Group Preprint Series, Department of Philosophy, Utrecht University, 1995.
   • J.F. Groote and J. Springintveld. Focus points and convergent process operators. A proof strategy for protocol verification. Technical Report 142, Logic Group Preprint Series, Utrecht University, 1995. This report also appeared as Technical Report CS-R9566, CWI, 1995
   • J.F. Groote and S.F.M. van Vlijmen. A modal logic for µCRL. In A. Ponse, M. de Rijke and Y. Venema, editors, Modal Logic and Process Algebra, a Bisimulation Perspective. CSLI Lecture Notes No. 53, pages 131-150, Stanford, 1995.
   • H.P. Korver and M.P.A. Sellink. On automating process algebra proofs. Technical Report 154. Logic Group Preprint Series, Utrecht University, 1996.
   • H.P. Korver and M.P.A. Sellink. Formalising LPOs and invariants in Coq. Technical Report 147. Logic Group Preprint Series, Utrecht University, 1995.
   • M.P.A. Sellink. Verifying process algebra proofs in type theory. In Andrews et al. Proceedings of the International Workshop on Semantics of Specification Languages. Workshops in Computing Series, pages 315-339. Springer-Verlag, 1994.

Top of page

4. Tools
   • D. Bosscher and A. Ponse. Translating a process algebra with symbolic data values to linear format. In U.H. Engberg, K.G. Larsen, and A. Skou, editors, Proceedings of the Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Aarhus 1995, BRICS Notes Series, pages 119-130. University of Aarhus, 1995.
   • D. Dams and J.F. Groote. Specification and implementation of components of a µCRL toolbox. Technical Report 152, Logic Group Preprint Series, Utrecht University, 1995.
   • J.A. Hillebrand and H.P. Korver. A well-formedness checker for µCRL. Technical Report P9501, University of Amsterdam, Programming Research Group, 1995. (Abstract)
   • H.P. Korver. Building a simulator in the µCRL toolbox. A case study in modern software engineering. Technical Report CS-R9632, CWI, Amsterdam, 1996. (Abstract)
   • I.A. van Langevelde. A compact file format for labeled transition systems. Technical Report SEN-R0102, CWI, Amsterdam, 2001. (Abstract)
   • J.C. van de Pol. A Prover for the muCRL toolset with applications -- version 0.1. Technical Report SEN-R0106, CWI, Amsterdam, 2001. (Abstract)

Top of page

5. Applications
   • M.A. Bezem and J.F. Groote. A formal verification of the alternating bit protocol in the calculus of constructions. Technical Report 88, Logic Group Preprint Series, Utrecht University, March 1993.
   • M.A. Bezem and J.F. Groote. A correctness proof of a one bit sliding window protocol in µCRL. The Computer Journal, 37(4): 289-307, 1994.
   • M.A. Bezem and A. Ponse. Two finite specifications of a queue. Technical Report P9424, University of Amsterdam, Programming Research Group, 1994. (Abstract)
   • L.-A. Fredlund, J.F. Groote and H.P. Korver. Formal verification of a leader election protocol in process algebra. Theoretical Computer Science, 177:459-486, 1997.
   • D. Griffioen and H.P. Korver. The Bakery Protocol: a comparative case-study in formal verification. Technical Report 136. Logic Group Preprint Series, Utrecht University, 1995.
   • J.F. Groote, J.W.C. Koorn and S.F.M. van Vlijmen. Formele analyse van het veiligheidssysteem op het station van Hoorn-Kersenboogerd. Informatie, Jaargang 36, nr. 6, pagina's 397-404, 1995.
   • J.F. Groote, J.W.C. Koorn and S.F.M. van Vlijmen. The safety guaranteeing system at station Hoorn-Kersenboogerd (Extended abstract). In Proceedings 10th Annual Conference on Computer Assurance (COMPASS'95), pp. 57-68, Gaithersburg, Maryland, 1995.
   • J.F. Groote and H.P. Korver. Correctness proof of the bakery protocol in µCRL. In A. Ponse, C. Verhoef and S.F.M. van Vlijmen, editors, Algebra of Communicating Processes '94, Workshops in Computing Series, pp. 63-86, Springer-Verlag, 1995.
   • J.F. Groote, F. Monin and J.C. van de Pol. Checking verifications of protocols and distributed systems by computer. In D. Sangiorgi and R. de Simone, editors, Proceedings of Concur'98, Sophia Antipolis, 1998. LNCS 1466, pages 629-655, Springer Verlag, 1998.
   • J.F. Groote and J.C. van de Pol. A bounded retransmission protocol for large data packets. A case study in computer checked verification. In M. Wirsing and M. Nivat, editors, Proceedings of AMAST'96, LNCS 1101, Springer Verlag, pages 536-550, 1996.
     Also appeared as Technical Report 100, Logic Group Preprint Series, Utrecht University, 1993.
   • H.P. Korver and M.P.A. Sellink. Example verifications using alphabet axioms. Formal Aspects of Computing, 10:43-58, 1998.
   • H.P. Korver and J. Springintveld. A computer-checked verification of Milner's scheduler. In M. Hagiya and J.C. Mitchell, editors, Proceedings of the International Symposium on Theoretical Aspects of Computer Software (TACS'94), LNCS 789, pages 161-178, Springer-Verlag, 1994.
     Also appeared as Technical Report 101 , Logic Group Preprint Series, Utrecht University, 1993.
   • S.P. Luttik. Description and formal specification of the link layer of P1394. Technical Report SEN-R9706, CWI, Amsterdam, 1997. (Abstract)
   • C. Shankland and M.B. van der Zwaag. The tree identify protocol of IEEE 1394 in µCRL. Formal Aspects of Computing, 10:509-531, 1998. Available as Technical Report SEN-R9831, CWI, Amsterdam, 1998. (Abstract).
   • Y.S. Usenko. A comparison of Spin and the muCRL toolset on HAVi leader election protocol. Technical Report SEN-R9917, CWI, Amsterdam}, 1999. (Abstract).

Top of page

6. Timed µCRL
   • J.F. Groote. The syntax and semantics of timed µCRL. Technical Report SEN-R9709, CWI, Amsterdam, 1997. (Abstract)
   • J.F. Groote, M.A. Reniers, J.J. van Wamel, and M.B. van der Zwaag. Completeness of timed muCRL. Technical Report SEN-R0034, CWI, Amsterdam, 2000. (Abstract)
   • J.F. Groote and J.J. van Wamel. Basic theorems for parallel processes in timed µCRL. Technical Report SEN-R9808, CWI, Amsterdam, 1998. ( Abstract)
   • J.F. Groote and J.J. van Wamel. Analysis of three hybrid systems in timed µCRL. Science of Computer Programming 39:215-247, 2001. Also available as Technical Report SEN-R9815, CWI, Amsterdam, 1998. (Abstract)
   • M.B. van der Zwaag. Time-stamped actions in pCRL algebras. Technical Report SEN-R0002, CWI, Amsterdam, 2000. (Abstract)
   • M.B. van der Zwaag. The cones and foci proof technique for timed transition systems. Technical Report SEN-R0038, CWI, Amsterdam, 2000. Accepted for publication in \emph{Information Processing Letters. (Abstract)

Top of page