{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,3]],"date-time":"2025-11-03T13:18:21Z","timestamp":1762175901498},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540614630"},{"type":"electronic","value":"9783540685951"}],"license":[{"start":{"date-parts":[[1996,1,1]],"date-time":"1996-01-01T00:00:00Z","timestamp":820454400000},"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":[[1996]]},"DOI":"10.1007\/bfb0014338","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T09:04:25Z","timestamp":1132736665000},"page":"536-550","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":33,"title":["A bounded retransmission protocol for large data packets"],"prefix":"10.1007","author":[{"given":"Jan Friso","family":"Groote","sequence":"first","affiliation":[]},{"given":"Jaco","family":"van de Pol","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"37_CR1","doi-asserted-by":"crossref","unstructured":"J.C.M. Baeten and W.P. Weijland. Process Algebra. Cambridge Tracts in Theoretical Computer Science 18. Cambridge University Press, 1990.","DOI":"10.1017\/CBO9780511624193"},{"key":"37_CR2","unstructured":"M. Bezem, R. Bol, and J.F. Groote. Formalizing process algebraic verifications in the calculus of constructions. Technical Report 95-02, Eindhoven University of Technology, January 1995. To appear in Formal Aspects of Computing."},{"issue":"4","key":"37_CR3","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1093\/comjnl\/37.4.289","volume":"37","author":"M.A. Bezem","year":"1994","unstructured":"M.A. Bezem and J.F. Groote. A correctness proof of a one-bit sliding window protocol in \u03bcCRL The Computer Journal, 37(4):289\u2013307, 1994.","journal-title":"The Computer Journal"},{"key":"37_CR4","unstructured":"G. Dowek, A. Felty, H. Herbelin, G. Huet, C. Murthy, C. Parent, C. Paulin-Mohring, and B. Werner. The Coq proof assistant user's guide. Version 5.8. Technical report, INRIA-Rocquencourt, May 1993."},{"key":"37_CR5","first-page":"63","volume-title":"Workshops in Computing","author":"J.F. Groote","year":"1994","unstructured":"J.F. Groote and H.P. Korver. A correctness proof of the bakery protocol in \u03bcCRL. In A. Ponse, C. Verhoef, and S.F.M. van Vlijmen, editors, Proc. 1st Workshop on the Algebra of Communicating Processes (ACP'94), Utrecht, Workshops in Computing, pages 63\u201386. Springer-Verlag, 1994."},{"key":"37_CR6","volume-title":"Technical Report CS-R9076","author":"J.F. Groote","year":"1990","unstructured":"J.F. Groote and A. Ponse. The syntax and semantics of \u03bcCRL. Technical Report CS-R9076, CWI, Amsterdam, December 1990."},{"key":"37_CR7","doi-asserted-by":"crossref","unstructured":"J.F. Groote and A. Ponse. Proof theory for \u03bcCRL: a language for processes with data. In D.J. Andrews, J.F. Groote, and C.A. Middelburg, editors, Proc. of the Int. Workshop on Semantics of Specification Languages, pages 232\u2013251. Workshops in Computing, Springer Verlag, 1994.","DOI":"10.1007\/978-1-4471-3229-5_13"},{"key":"37_CR8","unstructured":"J.F. Groote and J.C. van de Pol. A bounded retransmission protocol for large data packets. Technical Report Logic Group Preprint Series No. 100, Utrecht University, Oct 1993."},{"key":"37_CR9","doi-asserted-by":"crossref","unstructured":"K. Havelund and N. Shankar. Experiments in theorem proving and model checking for protocol verification. Obtainable via http:\/\/www.csl.sri.com\/\u223cshankar\/shankar.html, 1995.","DOI":"10.1007\/3-540-60973-3_113"},{"key":"37_CR10","doi-asserted-by":"crossref","unstructured":"L. Helmink, M.P.A. Sellink, and F.W. Vaandrager. Proof-checking a data link protocol. In H.P. Barendregt and T. Nipkow, editors, Proc. of the 1st International Workshop \u201cTypes for Proofs and Programs\u201d, May 1993, volume 806 of LNCS, pages 127\u2013165, Nijmegen, 1994.","DOI":"10.1007\/3-540-58085-9_75"},{"key":"37_CR11","unstructured":"ISO. Information processing systems \u2014 open systems interconnection \u2014 LOTOS \u2014 a formal description technique based on the temporal ordering of observational behaviour ISO IS 8807, 1989."},{"key":"37_CR12","first-page":"161","volume-title":"volume 789 of LNCS","author":"H. Korver","year":"1994","unstructured":"H. Korver and J. Springintveld. A computer-checked verification of Milner's scheduler. In M. Hagiya and J.C. Mitchell, editors, Proc. of the Int. Symp. on Theoretical Aspects of Computer Software, volume 789 of LNCS, pages 161\u2013178, Sendai, Japan, April 1994. Springer Verlag."},{"key":"37_CR13","unstructured":"S. Mauw. PSF\u2014A Process Specification Formalism. PhD thesis, University of Amsterdam, December 1991."},{"key":"37_CR14","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"R. Milner. Communication and Concurrency. Prentice-Hall International, Englewood Cliffs, 1989."},{"key":"37_CR15","first-page":"315","volume-title":"Verifying process algebra proofs in type theory","author":"M.P.A. Sellink","year":"1994","unstructured":"M.P.A. Sellink. Verifying process algebra proofs in type theory. In D.J. Andrews, J.F. Groote, and C.A. Middelburg, editors, Proc. of the Int. Workshop on Semantics of Specification Languages, Utrecht 1993, Workshops in Computing, pages 315\u2013339. Springer-Verlag, 1994."},{"key":"37_CR16","unstructured":"M.P.A. Sellink. Computer-Aided Verification of Protocols, The Type Theoretic Approach. Phd thesis, Utrecht University, February 1996."}],"container-title":["Lecture Notes in Computer Science","Algebraic Methodology and Software Technology"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0014338","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,9]],"date-time":"2020-01-09T04:36:14Z","timestamp":1578544574000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0014338"}},"subtitle":["A case study in computer checked algebraic verification"],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540614630","9783540685951"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/bfb0014338","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]},"assertion":[{"value":"9 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}