{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:45:22Z","timestamp":1772163922113,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":37,"publisher":"ACM","license":[{"start":{"date-parts":[[2005,8,22]],"date-time":"2005-08-22T00:00:00Z","timestamp":1124668800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2005,8,22]]},"DOI":"10.1145\/1080091.1080123","type":"proceedings-article","created":{"date-parts":[[2005,11,7]],"date-time":"2005-11-07T12:34:39Z","timestamp":1131366879000},"page":"265-276","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":38,"title":["Rigorous specification and conformance testing techniques for network protocols, as applied to TCP, UDP, and sockets"],"prefix":"10.1145","author":[{"given":"Steve","family":"Bishop","sequence":"first","affiliation":[{"name":"University of Cambridge Computer Laboratory"}]},{"given":"Matthew","family":"Fairbairn","sequence":"additional","affiliation":[{"name":"University of Cambridge Computer Laboratory"}]},{"given":"Michael","family":"Norrish","sequence":"additional","affiliation":[{"name":"NICTA, Canberra"}]},{"given":"Peter","family":"Sewell","sequence":"additional","affiliation":[{"name":"University of Cambridge Computer Laboratory"}]},{"given":"Michael","family":"Smith","sequence":"additional","affiliation":[{"name":"University of Cambridge Computer Laboratory"}]},{"given":"Keith","family":"Wansbrough","sequence":"additional","affiliation":[{"name":"University of Cambridge Computer Laboratory"}]}],"member":"320","published-online":{"date-parts":[[2005,8,22]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/647770.734114"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/774763.774783"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360221"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/581771.581775"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/190314.190318"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/783106.783122"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/90.649465"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36577-X_9"},{"key":"e_1_3_2_1_11_1","first-page":"21","volume-title":"Proc. 11th CATS, Computing: The Australasian Theory Symposium","author":"Compton M.","year":"2005","unstructured":"M. Compton . Stenning's protocol implemented in UDP and verified in Isabelle . In Proc. 11th CATS, Computing: The Australasian Theory Symposium , pages 21 -- 30 , 2005 .]] M. Compton. Stenning's protocol implemented in UDP and verified in Isabelle. In Proc. 11th CATS, Computing: The Australasian Theory Symposium, pages 21--30, 2005.]]"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/645880.672086"},{"key":"e_1_3_2_1_13_1","unstructured":"Fyodor. nmap. http:\/\/www.insecure.org\/nmap\/.]]  Fyodor. nmap. http:\/\/www.insecure.org\/nmap\/.]]"},{"key":"e_1_3_2_1_14_1","volume-title":"Introduction to HOL: a theorem proving environment","author":"Gordon M. J. C.","year":"1993","unstructured":"M. J. C. Gordon and T. Melham , editors . Introduction to HOL: a theorem proving environment . Cambridge University Press , 1993 .]] M. J. C. Gordon and T. Melham, editors. Introduction to HOL: a theorem proving environment. Cambridge University Press, 1993.]]"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/646483.691600"},{"key":"e_1_3_2_1_16_1","volume-title":"Proc. 8th Euromicro Workshop on Parallel and Distributed Processing","author":"Hofmann R.","year":"2000","unstructured":"R. Hofmann and F. Lemmen . Specification-driven monitoring of TCP\/IP . In Proc. 8th Euromicro Workshop on Parallel and Distributed Processing , Jan. 2000 .]] R. Hofmann and F. Lemmen. Specification-driven monitoring of TCP\/IP. In Proc. 8th Euromicro Workshop on Parallel and Distributed Processing, Jan. 2000.]]"},{"key":"e_1_3_2_1_17_1","unstructured":"The HOL 4 system Kananaskis-2 release. http:\/\/hol.sourceforge.net\/.]]  The HOL 4 system Kananaskis-2 release. http:\/\/hol.sourceforge.net\/.]]"},{"key":"e_1_3_2_1_18_1","unstructured":"IEEE and The Open Group. IEEE Std 1003.1 TM -2001 Standard for Information Technology - Portable Operating System Interface (POSIX\u00ae). Dec. 2001. Issue 6. Available http:\/\/www.opengroup.org\/onlinepubs\/007904975\/toc.htm.]]  IEEE and The Open Group. IEEE Std 1003.1 TM -2001 Standard for Information Technology - Portable Operating System Interface (POSIX\u00ae). Dec. 2001. Issue 6. Available http:\/\/www.opengroup.org\/onlinepubs\/007904975\/toc.htm.]]"},{"key":"e_1_3_2_1_19_1","unstructured":"The Isabelle proof assistant. http:\/\/isabelle.in.tum.de\/.]]  The Isabelle proof assistant. http:\/\/isabelle.in.tum.de\/.]]"},{"key":"e_1_3_2_1_20_1","unstructured":"IXIA. IxANVL(\u2122)-automated network validation library 2005. http:\/\/www.ixiacom.com\/.]]  IXIA. IxANVL(\u2122)-automated network validation library 2005. http:\/\/www.ixiacom.com\/.]]"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/316188.316200"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004854"},{"key":"e_1_3_2_1_23_1","volume-title":"INRIA","author":"Leroy X.","year":"2004","unstructured":"X. Leroy The Objective-Caml System, Release 3.08.2 . INRIA , Nov. 2004 . Available http:\/\/caml.inria.fr\/.]] X. Leroy et al. The Objective-Caml System, Release 3.08.2. INRIA, Nov. 2004. Available http:\/\/caml.inria.fr\/.]]"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/55482.55495"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/52324.52334"},{"key":"e_1_3_2_1_26_1","first-page":"155","volume-title":"Proc.NSDI: 1st Symposium on Networked Systems Design and Implementation","author":"Musuvathi M.","year":"2004","unstructured":"M. Musuvathi and D. Engler . Model checking large network protocol implementations . In Proc.NSDI: 1st Symposium on Networked Systems Design and Implementation , pages 155 -- 168 , 2004 .]] M. Musuvathi and D. Engler. Model checking large network protocol implementations. In Proc.NSDI: 1st Symposium on Networked Systems Design and Implementation, pages 155--168, 2004.]]"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133373.1133383"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/383059.383083"},{"key":"e_1_3_2_1_29_1","volume-title":"Aug.","author":"Parker S.","year":"1998","unstructured":"S. Parker and C. Schmechel . RFC2398: Some testing tools for TCP implementors , Aug. 1998 .]] S. Parker and C. Schmechel. RFC2398: Some testing tools for TCP implementors, Aug. 1998.]]"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/263105.263160"},{"key":"e_1_3_2_1_31_1","volume-title":"Computer Science Department","author":"Postel J.","year":"1974","unstructured":"J. Postel . A Graph Model Analysis of Computer Communications Protocols. University of California , Computer Science Department , PhD Thesis , 1974 .]] J. Postel. A Graph Model Analysis of Computer Communications Protocols. University of California, Computer Science Department, PhD Thesis, 1974.]]"},{"key":"e_1_3_2_1_32_1","volume-title":"Proc. COST 247 International Workshop on Applied Formal Methods In System Design","author":"Schieferdecker I.","year":"1996","unstructured":"I. Schieferdecker . Abruptly-terminated connections in TCP -- a verification example . In Proc. COST 247 International Workshop on Applied Formal Methods In System Design , June 1996 .]] I. Schieferdecker. Abruptly-terminated connections in TCP -- a verification example. In Proc. COST 247 International Workshop on Applied Formal Methods In System Design, June 1996.]]"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/645870.668688"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/90.993301"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/277467.277477"},{"key":"e_1_3_2_1_37_1","volume-title":"1: The Protocols","author":"Stevens W. R.","year":"1994","unstructured":"W. R. Stevens . TCP\/ IP Illustrated Vol . 1: The Protocols . 1994 .]] W. R. Stevens. TCP\/IP Illustrated Vol. 1: The Protocols. 1994.]]"},{"key":"e_1_3_2_1_38_1","volume-title":"1: Networking APIs: Sockets and XTI","author":"Stevens W. R.","year":"1998","unstructured":"W. R. Stevens . UNIX Network Programming Vol . 1: Networking APIs: Sockets and XTI . Second edition, 1998 .]] W. R. Stevens. UNIX Network Programming Vol. 1: Networking APIs: Sockets and XTI. Second edition, 1998.]]"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.5555\/645396.651956"},{"key":"e_1_3_2_1_40_1","volume-title":"The Implementation.","author":"Wright G. R.","year":"1995","unstructured":"G. R. Wright and W. R. Stevens . TCP\/IP Illustrated Vol. 2 : The Implementation. 1995 .]] G. R. Wright and W. R. Stevens. TCP\/IP Illustrated Vol. 2: The Implementation. 1995.]]"}],"event":{"name":"SIGCOMM05: ACM SIGCOMM 2005 Conference","location":"Philadelphia Pennsylvania USA","acronym":"SIGCOMM05","sponsor":["SIGCOMM ACM Special Interest Group on Data Communication","ACM Association for Computing Machinery"]},"container-title":["Proceedings of the 2005 conference on Applications, technologies, architectures, and protocols for computer communications"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1080091.1080123","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1080091.1080123","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T12:08:26Z","timestamp":1750248506000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1080091.1080123"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,8,22]]},"references-count":37,"alternative-id":["10.1145\/1080091.1080123","10.1145\/1080091"],"URL":"https:\/\/doi.org\/10.1145\/1080091.1080123","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1090191.1080123","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2005,8,22]]},"assertion":[{"value":"2005-08-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}