{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:31:40Z","timestamp":1725492700478},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540433637"},{"type":"electronic","value":"9783540459279"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45927-8_20","type":"book-chapter","created":{"date-parts":[[2007,10,19]],"date-time":"2007-10-19T09:39:04Z","timestamp":1192786744000},"page":"278-294","source":"Crossref","is-referenced-by-count":2,"title":["Timing UDP: Mechanized Semantics for Sockets, Threads, and Failures"],"prefix":"10.1007","author":[{"given":"Keith","family":"Wansbrough","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Norrish","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Sewell","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrei","family":"Serjantov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,3,14]]},"reference":[{"issue":"1","key":"20_CR1","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0304-3975(98)00235-7","volume":"220","author":"M. K. Aguilera","year":"1999","unstructured":"M. K. Aguilera, W. Chen, and S. Toueg. Using the heartbeat failure detector for quiescent reliable communication and consensus in partitionable networks. Theoretical Computer Science, 220(1):3\u201330, June 1999.","journal-title":"Theoretical Computer Science"},{"key":"20_CR2","doi-asserted-by":"crossref","unstructured":"T. Arts and M. Dam. Verifying a distributed database lookup manager written in Erlang. In World Congress on Formal Methods (1), 1999.","DOI":"10.1007\/3-540-48119-2_38"},{"key":"20_CR3","doi-asserted-by":"crossref","unstructured":"F. Baker. Requirements for IP version 4 routers, RFC 1812. Internet Engineering Task Force, June 1995. http:\/\/www.ietf.org\/rfc.html .","DOI":"10.17487\/rfc1812"},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"K. Bhargavan, S. Chandra, P. J. McCann, and C. A. Gunter. What packets may come: Automata for network monitoring. In Proc. POPL 2001.","DOI":"10.1145\/360204.360221"},{"key":"20_CR5","doi-asserted-by":"crossref","unstructured":"R. Braden. Requirements for internet hosts \u2014 communication layers, STD 3, RFC 1122. Internet Engineering Task Force, October 1989.","DOI":"10.17487\/rfc1122"},{"key":"20_CR6","unstructured":"University of California at Berkeley CSRG. 4.2BSD, 1983."},{"key":"20_CR7","unstructured":"S. J. Garland, N. Lynch, and M. Vaziri. IOA reference guide, December 2000. http:\/\/nms.lcs.mit.edu\/~garland\/IOA\/ ."},{"key":"20_CR8","unstructured":"M. J. C. Gordon and T. Melham, editors. Introduction to HOL: a theorem proving environment. Cambridge University Press, 1993."},{"key":"20_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1007\/BFb0057019","volume-title":"An object calculus for asynchronous communication","author":"K. Honda","year":"1991","unstructured":"K. Honda and M. Tokoro. An object calculus for asynchronous communication. In Proceedings of ECOOP\u2019 91, LNCS 512, pages 133\u2013147, 1991."},{"key":"20_CR10","unstructured":"[IEE00] IEEE. Portable Operating System Interface (POSIX)-Part xx: Protocol Independent Interfaces (PII), P1003.1g. March 2000."},{"key":"20_CR11","unstructured":"X. Leroy et al. The Objective-Caml System, Release 3.02. INRIA, July 30 2001. Available http:\/\/caml.inria.fr\/ocaml\/ ."},{"issue":"1","key":"20_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1996.0060","volume":"128","author":"N. Lynch","year":"1996","unstructured":"N. Lynch and F. Vaandrager. Forward and backward simulations-Part II: Timing-based systems. Information and Computation, 128(1):1\u201325, 1996.","journal-title":"Information and Computation"},{"key":"20_CR13","unstructured":"M. Norrish. C formalised in HOL. PhD thesis, Computer Laboratory, University of Cambridge, 1998."},{"key":"20_CR14","doi-asserted-by":"crossref","unstructured":"M. Norrish and K. Slind. A thread of HOL development. Computer Journal, 2002. To appear.","DOI":"10.1093\/comjnl\/45.1.37"},{"key":"20_CR15","doi-asserted-by":"crossref","unstructured":"J. Postel. User Datagram Protocol, STD 6, RFC 768. Internet Engineering Task Force, August 1980. http:\/\/www.ietf.org\/rfc.html .","DOI":"10.17487\/rfc0768"},{"key":"20_CR16","doi-asserted-by":"crossref","unstructured":"J. Postel. Internet Protocol, STD 5, RFC 791. Internet Engineering Task Force, September 1981. http:\/\/www.ietf.org\/rfc.html .","DOI":"10.17487\/rfc0791"},{"key":"20_CR17","unstructured":"I. Schieferdecker. Abruptly terminated connections in TCP \u2014 a verification example. In Proc. COST 247 International Workshop on Applied Formal Methods in System Design, pages 136\u2013145, 1996."},{"key":"20_CR18","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1006\/inco.1997.2671","volume":"141","author":"R. Segala","year":"1998","unstructured":"R. Segala, R. Gawlick, J. S\u00f8gaard-Andersen, and N. Lynch. Liveness in timed and untimed systems. Inf. and Comp., 141:119\u2013171, 1998.","journal-title":"Inf. and Comp."},{"key":"20_CR19","doi-asserted-by":"crossref","unstructured":"M. Smith. Formal verification of communication protocols. In FORTE\/PSTV\u201996, pages 129\u2013144, 1996.","DOI":"10.1007\/978-0-387-35079-0_8"},{"key":"20_CR20","doi-asserted-by":"crossref","unstructured":"A. Serjantov, P. Sewell, and K. Wansbrough. The UDP calculus: Rigorous semantics for real networking. In Proc TACS2001, Sendai, October 2001.","DOI":"10.1007\/3-540-45500-0_27"},{"key":"20_CR21","doi-asserted-by":"crossref","unstructured":"A. Serjantov, P. Sewell, and K. Wansbrough. The UDP calculus: Rigorous semantics for real networking. TR 515, Computer Laboratory, University of Cambridge, July 2001. http:\/\/www.cl.cam.ac.uk\/users\/pes20\/Netsem\/ .","DOI":"10.1007\/3-540-45500-0_27"},{"key":"20_CR22","unstructured":"W. R. Stevens. TCP\/IP Illustrated Vol. 1: The Protocols. Addison-Wesley, 1994."},{"key":"20_CR23","unstructured":"W. R. Stevens. UNIX Network Programming Vol. 1: Networking APIs: Sockets and XTI. Prentice Hall, second edition, 1998."},{"key":"20_CR24","unstructured":"M. VanInwegen. The machine-assisted proof of programming language properties. PhD thesis, University of Pennsylvania, December 1996."},{"key":"20_CR25","unstructured":"K. Wansbrough, M. Norrish, P. Sewell, and A. Serjantov. Timing UDP: the HOL model, 2001. http:\/\/www.cl.cam.ac.uk\/users\/pes20\/Netsem\/ ."},{"key":"20_CR26","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1007\/3-540-54233-7_136","volume-title":"CCS + time = an interleaving model for real time systems","author":"W. Yi","year":"1991","unstructured":"W. Yi. CCS + time = an interleaving model for real time systems. In Proc. ICALP 1991, LNCS 510, pages 217\u2013228, 1991."}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45927-8_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T21:29:09Z","timestamp":1556918949000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45927-8_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540433637","9783540459279"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-45927-8_20","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}