{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:18:37Z","timestamp":1725495517762},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540664253"},{"type":"electronic","value":"9783540483205"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48320-9_36","type":"book-chapter","created":{"date-parts":[[2007,11,15]],"date-time":"2007-11-15T08:52:42Z","timestamp":1195116762000},"page":"525-540","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Proof-Checking Protocols Using Bisimulations"],"prefix":"10.1007","author":[{"given":"Christine","family":"R\u00f6ckl","sequence":"first","affiliation":[]},{"given":"Javier","family":"Esparza","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,4,19]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"J. Baeten and W. Weijland. Process Algebra. Cambridge University Press, 1990.","key":"36_CR1","DOI":"10.1017\/CBO9780511624193"},{"issue":"5","key":"36_CR2","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1145\/362946.362970","volume":"12","author":"K. A. Bartlett","year":"1969","unstructured":"K. A. Bartlett, R. A. Scantlebury, and P. T. Wilkinson. A note on reliable fullduplex transmission over half-duplex links. Comm. of the ACM, 12(5):260\u2013261, May 1969.","journal-title":"Comm. of the ACM"},{"key":"36_CR3","series-title":"Lect Notes Comput Sci","volume-title":"Mathematical Methods of Specification and Synthesis of Software Systems\u2019 85","author":"J. A. Bergstra","year":"1985","unstructured":"J. A. Bergstra and J. W. Klop. Verification of an alternating bit protocol by means of process algebra. In Mathematical Methods of Specification and Synthesis of Software Systems\u2019 85, volume 215 of LNCS. Springer, 1985."},{"unstructured":"M. Bezem and J. F. Groote. A formal verification of the alternating bit protocol in the calculus of constructions. Logic Group Preprint Series 88, Dept. of Philosophy, Utrecht University, 1993.","key":"36_CR4"},{"key":"36_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/3-540-61780-9_67","volume-title":"Proc. TYPES\u201995","author":"E. Gimenez","year":"1996","unstructured":"E. Gimenez. An application of co-inductive types in Coq: Verification of the alternating bit protocol. In Proc. TYPES\u201995, volume 1158 of LNCS, pages 135\u2013152. Springer, 1996."},{"unstructured":"J. F. Groote and J. G. Springintveld. Focus points and convergent process operators. Logic Group Preprint Series 142, Dept. of Philosophy, Utrecht University, 1995.","key":"36_CR6"},{"unstructured":"J. F. Groote and J. G. Springintveld. Algebraic verification of a distributed summation algorithm. Technical Report CS-R9640, CWI, Amsterdam, 1996.","key":"36_CR7"},{"unstructured":"T. Hardin and B. Mammass. Proving the bounded retransmission protocol in the pi-calculus. In Proc. INFINITY\u201998, 1998.","key":"36_CR8"},{"unstructured":"R. Milner. Communication and Concurrency. Prentice-Hall, 1989.","key":"36_CR9"},{"key":"36_CR10","series-title":"Lect Notes Comput Sci","volume-title":"Proc. CONCUR\u201992","author":"R. Milner","year":"1992","unstructured":"R. Milner and D. Sangiorgi. The problem of weak bisimulation up-to. In Proc. CONCUR\u201992, volume 630 of LNCS. Springer, 1992."},{"key":"36_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"284","DOI":"10.1007\/BFb0058037","volume-title":"Proc. FSTTCS\u201997","author":"K. Namjoshi","year":"1997","unstructured":"K. Namjoshi. A simple characterization of stuttering bisimulation. In Proc. FSTTCS\u201997, volume 1346 of LNCS, pages 284\u2013296. Springer, 1997."},{"key":"36_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"648","DOI":"10.1007\/3-540-60084-1_112","volume-title":"Proc. ICALP\u201995","author":"V. Natarajan","year":"1995","unstructured":"V. Natarajan and R. Cleaveland. Divergence and fair testing. In Proc. ICALP\u201995, volume 944 of LNCS, pages 648\u2013659. Springer, 1995."},{"key":"36_CR13","series-title":"Lect Notes Comput Sci","first-page":"101","volume-title":"Proc. TYPES\u201994","author":"T. Nipkow","year":"1994","unstructured":"T. Nipkow and K. Slind. I\/O automata in Isabelle\/HOL. In Proc. TYPES\u201994, volume 996 of LNCS, pages 101\u2013119. Springer, 1994."},{"unstructured":"K. Paliwoda and J. Sanders. The sliding-window protocol. Technical Report PRG66, Programming Research Group, Oxford University, March 1988.","key":"36_CR14"},{"doi-asserted-by":"crossref","unstructured":"L. C. Paulson. Isabelle\u2019s object-logics. Technical Report 286, University of Cambridge, Computer Laboratory, 1993.","key":"36_CR15","DOI":"10.1007\/BFb0030541"},{"key":"36_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: a generic theorem prover","author":"L. C. Paulson","year":"1994","unstructured":"L. C. Paulson. Isabelle: a generic theorem prover, volume 828 of LNCS. Springer, 1994."},{"unstructured":"G. Plotkin. Structural operational semantics. Technical report, DAIMI, Aarhus University, 1981.","key":"36_CR17"},{"key":"36_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"479","DOI":"10.1007\/3-540-60246-1_153","volume-title":"Proc. MFCS\u201995","author":"D. Sangiorgi","year":"1995","unstructured":"D. Sangiorgi. On the proof method for bisimulation. In Proc. MFCS\u201995, volume 969 of LNCS, pages 479\u2013488. Springer, 1995."},{"key":"36_CR19","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/BF01214620","volume":"7","author":"J. L. A. Snepscheut","year":"1995","unstructured":"J. L. A. Snepscheut. The sliding-window protocol revisited. Formal Aspects of Computing, 7:3\u201317, 1995.","journal-title":"Formal Aspects of Computing"},{"issue":"2","key":"36_CR20","doi-asserted-by":"publisher","first-page":"202241","DOI":"10.1016\/0890-5401(90)90048-M","volume":"85","author":"D. Walker","year":"1990","unstructured":"D. Walker. Bisimulation and divergence. Information and Computation, 85(2):202241, 1990.","journal-title":"Information and Computation"}],"container-title":["Lecture Notes in Computer Science","CONCUR\u201999 Concurrency Theory"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48320-9_36","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T11:09:26Z","timestamp":1558264166000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48320-9_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540664253","9783540483205"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-48320-9_36","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]},"assertion":[{"value":"19 April 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}