{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:49:45Z","timestamp":1762458585334},"reference-count":52,"publisher":"Elsevier","isbn-type":[{"value":"9780444828309","type":"print"}],"license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1016\/b978-044482830-9\/50035-7","type":"book-chapter","created":{"date-parts":[[2007,10,10]],"date-time":"2007-10-10T17:58:36Z","timestamp":1192039116000},"page":"1151-1208","source":"Crossref","is-referenced-by-count":36,"title":["Algebraic Process Verification"],"prefix":"10.1016","author":[{"given":"J.F.","family":"Groote","sequence":"first","affiliation":[]},{"given":"M.A.","family":"Reniers","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/B978-044482830-9\/50035-7_bib1","series-title":"The Lambda Calculus","author":"Barendregt","year":"1981"},{"key":"10.1016\/B978-044482830-9\/50035-7_bib2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF01212523","article-title":"Formalizing process algebraic verifications in the calculus of constructions","volume":"9","author":"Bezem","year":"1997","journal-title":"Formal Aspects of Comput."},{"key":"10.1016\/B978-044482830-9\/50035-7_bib3","article-title":"Towards a mathematical theory of processes","author":"Beki","year":"1971","journal-title":"Technical Report TR25.125, IBM Laboratory, Vienna"},{"issue":"4","key":"10.1016\/B978-044482830-9\/50035-7_bib4","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1093\/comjnl\/37.4.289","article-title":"A correctness proof of a one-bit sliding window protocol in \u03bcCRL","volume":"37","author":"Bezem","year":"1994","journal-title":"The Comput. J."},{"key":"10.1016\/B978-044482830-9\/50035-7_bib5","series-title":"CONCUR'94: Concurrency Theory","first-page":"401","article-title":"Invariants in process algebra with data","author":"Bezem","year":"1994"},{"key":"10.1016\/B978-044482830-9\/50035-7_bib6","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1016\/S0167-6423(96)00035-4","article-title":"Grid protocols based on synchronous communication","volume":"29","author":"Bergstra","year":"1997","journal-title":"Sci. Comput. Programming"},{"issue":"1\u20133","key":"10.1016\/B978-044482830-9\/50035-7_bib7","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1016\/S0019-9958(84)80025-X","article-title":"Process algebra for synchronous communication","volume":"60","author":"Bergstra","year":"1984","journal-title":"Inform. and Control"},{"key":"10.1016\/B978-044482830-9\/50035-7_bib8","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624193","article-title":"Process Algebra","author":"Baeten","year":"1990"},{"key":"10.1016\/B978-044482830-9\/50035-7_bib9","series-title":"Parallel Program Design: A Foundation","author":"Chandy","year":"1989"},{"key":"10.1016\/B978-044482830-9\/50035-7_bib10","series-title":"\u03bcCRL: A language and toolset to study communicating processes with data","author":"CWI","year":"2000"},{"key":"10.1016\/B978-044482830-9\/50035-7_bib11","series-title":"Control Flow Semantics","author":"de Bakker","year":"1996"},{"key":"10.1016\/B978-044482830-9\/50035-7_bib12","article-title":"The Coq proof assistant user's guide, Version 5.9","author":"Dowek","year":"1993","journal-title":"Technical Report, INRIA-Rocquencourt and CNRS-ENS Lyon"},{"key":"10.1016\/B978-044482830-9\/50035-7_bib13","article-title":"Verification of a leader election protocol \u2013 formal methods applied to IEEE 1394","author":"Devillers","year":"1997","journal-title":"Technical Report, Computing Science Institute, University of Nijmegen"},{"key":"10.1016\/B978-044482830-9\/50035-7_bib14","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-69962-7","article-title":"Fundamentals of Algebraic Specification: Equations and Initial Semantics","author":"Ehrig","year":"1985"},{"key":"10.1016\/B978-044482830-9\/50035-7_bib15","series-title":"Proc. CAV'96","first-page":"437","article-title":"CADP (CAE-SAR?ALDEBARAN Development Package): A protocol validation and verification toolbox","author":"Fernandez","year":"1996"},{"key":"10.1016\/B978-044482830-9\/50035-7_bib16","doi-asserted-by":"crossref","first-page":"459","DOI":"10.1016\/S0304-3975(96)00256-3","article-title":"Formal verification of a leader election protocol in process algebra","volume":"177","author":"Fredlund","year":"1997","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/B978-044482830-9\/50035-7_bib17","series-title":"Algebra of Communicating Processes, Workshops in Computing","first-page":"63","article-title":"Correctness proof of the bakery protocol in \u03bcCRL","author":"Groote","year":"1994"},{"key":"10.1016\/B978-044482830-9\/50035-7_bib18","article-title":"A computer checked algebraic verification of a distributed summing protocol","author":"Groote","year":"1997","journal-title":"Technical Report 97\/14, Department of Mathematics and Computing Science, Eindhoven University of Technology"},{"key":"10.1016\/B978-044482830-9\/50035-7_bib19","series-title":"Proc. CONCUR'98, Sophia Antipolis","first-page":"629","article-title":"Checking verifications of protocols and distributed systems by computer","author":"Groote","year":"1998"},{"key":"10.1016\/B978-044482830-9\/50035-7_bib20","series-title":"Semantics of Specification Languages, Proccedings of the International Workshop on Semantics of Specification Languages","first-page":"232","article-title":"Proof theory for \u03bcCRL: A language for processes with data","author":"Groote","year":"1994"},{"key":"10.1016\/B978-044482830-9\/50035-7_bib21","series-title":"Algebra of Communicating Processes, Utrecht 1994, Workshops in Computing","first-page":"26","article-title":"The syntax and semantics of \u03bcCRL","author":"Groote","year":"1995"},{"key":"10.1016\/B978-044482830-9\/50035-7_bib22","series-title":"ERCIM Workshop on Formal Methods for Industrial Critical Systems","first-page":"65","article-title":"A note on n similar parallel processes","author":"Groote","year":"1997"},{"key":"10.1016\/B978-044482830-9\/50035-7_bib23","article-title":"The syntax and semantics of timed \u03bcCRL","author":"Groote","year":"1997","journal-title":"Technical Report SEN-R9709, CWI, Amsterdam"},{"key":"10.1016\/B978-044482830-9\/50035-7_bib24","article-title":"Focus points and convergent process operators. A proof strategy for protocol verification","author":"Groote","year":"1995","journal-title":"Technical Report 142, University Utrecht, Department of Philosophy"},{"issue":"1\u20132","key":"10.1016\/B978-044482830-9\/50035-7_bib25","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1016\/S0304-3975(96)80702-X","article-title":"Confluence for process verification","volume":"170","author":"Groote","year":"1996","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/B978-044482830-9\/50035-7_bib26","series-title":"Proc. AMAST'96","first-page":"536","article-title":"A bounded retransmission protocol for large data packets. A case study in computer checked verification","author":"Groote","year":"1996"},{"key":"10.1016\/B978-044482830-9\/50035-7_bib27","doi-asserted-by":"crossref","DOI":"10.1145\/359576.359585","article-title":"Communicating Sequential Processes","author":"Hoare","year":"1985"},{"key":"10.1016\/B978-044482830-9\/50035-7_bib28","series-title":"Proc. FORTE '94","article-title":"An improvement in formal verification","author":"Holzmann","year":"1994"},{"key":"10.1016\/B978-044482830-9\/50035-7_bib29","series-title":"IEEE Standard for a high performance serial bus","author":"IEEE Computer Society","year":"1996"},{"key":"10.1016\/B978-044482830-9\/50035-7_bib30","series-title":"Recommendation Z.100: Specification and Description Language (SDL)","author":"ITU-T","year":"1994"},{"key":"10.1016\/B978-044482830-9\/50035-7_bib31","article-title":"Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use","author":"Jensen","year":"1992"},{"key":"10.1016\/B978-044482830-9\/50035-7_bib32","series-title":"Proc. 2nd IEEE Conference on Formal Engineering Methods","first-page":"90","article-title":"A process algebra based verification of a production system","author":"Kleijn","year":"1998"},{"key":"10.1016\/B978-044482830-9\/50035-7_bib33","series-title":"Proc. Internat. Symposium on Theoretical Aspects of Computer Software (TACS'94)","first-page":"161","article-title":"A computer-checked verification of Milner's scheduler","author":"Korver","year":"1994"},{"key":"10.1016\/B978-044482830-9\/50035-7_bib34","article-title":"Description and formal specification of the link layer of P1394","author":"Luttik","year":"1997","journal-title":"Technical Report SEN-R9706, CWI, Amsterdam"},{"key":"10.1016\/B978-044482830-9\/50035-7_bib35","series-title":"Distributed Algorithms","author":"Lynch","year":"1996"},{"key":"10.1016\/B978-044482830-9\/50035-7_bib36","series-title":"Linear Time, Branching Time and Partial Orders in Logics and Models for Concurrency","first-page":"285","article-title":"Basic notions of trace theory","author":"Mazurkiewicz","year":"1988"},{"key":"10.1016\/B978-044482830-9\/50035-7_bib37","series-title":"Proceedings Logic Colloquium 1973","first-page":"158","article-title":"A mathematical model of computing agents","author":"Milner","year":"1973"},{"key":"10.1016\/B978-044482830-9\/50035-7_bib38","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-10235-3","article-title":"A Calculus of Communicating Systems","author":"Milner","year":"1980"},{"key":"10.1016\/B978-044482830-9\/50035-7_bib39","article-title":"Communication and Concurrency","author":"Milner","year":"1989"},{"key":"10.1016\/B978-044482830-9\/50035-7_bib40","doi-asserted-by":"crossref","first-page":"85","DOI":"10.3233\/FI-1990-13202","article-title":"A process specification formalism","volume":"XIII","author":"Mauw","year":"1990","journal-title":"Fundamenta Informaticae"},{"key":"10.1016\/B978-044482830-9\/50035-7_bib41","series-title":"Logic and Computer Science","first-page":"361","article-title":"Isabelle: the next 700 theorem provers","author":"Paulson","year":"1990"},{"key":"10.1016\/B978-044482830-9\/50035-7_bib42","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","article-title":"Isabelle: A Generic Theorem Prover","author":"Paulson","year":"1994"},{"key":"10.1016\/B978-044482830-9\/50035-7_bib43","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1016\/0304-3975(87)90117-4","article-title":"Refusal testing","volume":"50","author":"Phillips","year":"1987","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/B978-044482830-9\/50035-7_bib44","series-title":"CONCUR'91, Proc. 2nd International Conference on Concurrency Theory","first-page":"471","article-title":"Efficient verification of determinate processes","author":"Qin","year":"1991"},{"key":"10.1016\/B978-044482830-9\/50035-7_bib45","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-69968-9","article-title":"Petri Nets: An Introduction","author":"Reisig","year":"1985"},{"key":"10.1016\/B978-044482830-9\/50035-7_bib46","article-title":"Validation of the link layer protocol of the IEEE-1394 serial bus (FireWire): An experiment with E-LOTOS","author":"Sighireanu","year":"1997","journal-title":"Technical Report 3172, INRIA"},{"key":"10.1016\/B978-044482830-9\/50035-7_bib47","article-title":"The PVS proof checker: A reference manual","author":"Shankar","year":"1993","journal-title":"Technical Report, Computer Science Laboratory, SRI International, Menlo Park, CA"},{"key":"10.1016\/B978-044482830-9\/50035-7_bib48","doi-asserted-by":"crossref","first-page":"509","DOI":"10.1007\/s001650050030","article-title":"The tree identify protocol of IEEE 1394 in \u03bcCRL","volume":"10","author":"Shankland","year":"1998","journal-title":"Formal Aspects of Comput."},{"key":"10.1016\/B978-044482830-9\/50035-7_bib49","series-title":"CONCUR'90 \u2013 Theories of Concurrency: Unification and Extension, Amsterdam","first-page":"278","article-title":"The linear time \u2013 branching time spectrum","author":"van Glabbeek","year":"1990"},{"key":"10.1016\/B978-044482830-9\/50035-7_bib50","series-title":"CONCUR'93, Proc. International Conference on Concurrency Theory","first-page":"66","article-title":"The linear time \u2013 branching time spectrum II. The semantics of sequential processes with silent moves","author":"van Glabbeek","year":"1993"},{"key":"10.1016\/B978-044482830-9\/50035-7_bib51","article-title":"Verification techniques for elementary data types and retransmission protocols","author":"van Wamel","year":"1995","journal-title":"Ph.D. Thesis, University of Amsterdam"},{"key":"10.1016\/B978-044482830-9\/50035-7_bib52","series-title":"Petri Nets: Applications and Relationships to Other Models of Concurrency","first-page":"325","article-title":"Event structures","author":"Winskel","year":"1987"}],"container-title":["Handbook of Process Algebra"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780444828309500357?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780444828309500357?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2021,8,25]],"date-time":"2021-08-25T16:43:37Z","timestamp":1629909817000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/B9780444828309500357"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9780444828309"],"references-count":52,"URL":"https:\/\/doi.org\/10.1016\/b978-044482830-9\/50035-7","relation":{},"subject":[],"published":{"date-parts":[[2001]]}}}