{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:30:11Z","timestamp":1774837811369,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":26,"publisher":"ACM","license":[{"start":{"date-parts":[[2006,1,11]],"date-time":"2006-01-11T00:00:00Z","timestamp":1136937600000},"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":[[2006,1,11]]},"DOI":"10.1145\/1111037.1111043","type":"proceedings-article","created":{"date-parts":[[2006,2,6]],"date-time":"2006-02-06T10:52:40Z","timestamp":1139223160000},"page":"55-66","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":23,"title":["Engineering with logic"],"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":[[2006,1,11]]},"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\/360204.360221"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/581771.581775"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/190314.190318"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1080091.1080123"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/90.649465"},{"key":"e_1_3_2_1_9_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_10_1","volume-title":"LNCS 78.","author":"Gordon M.","year":"1979","unstructured":"M. Gordon , R. Milner , and C. P. Wadsworth . Edinburgh LCF , LNCS 78. 1979 .]] M. Gordon, R. Milner, and C. P. Wadsworth. Edinburgh LCF, LNCS 78. 1979.]]"},{"key":"e_1_3_2_1_11_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_12_1","unstructured":"The HOL 4 system Kananaskis-3 release. hol.sourceforge.net.]]  The HOL 4 system Kananaskis-3 release. hol.sourceforge.net.]]"},{"key":"e_1_3_2_1_13_1","unstructured":"IEEE and The Open Group. IEEE Std 1003.1\u2122-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\u2122-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_14_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_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/316188.316200"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0060"},{"key":"e_1_3_2_1_17_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_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133373.1133383"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/263105.263160"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/645870.668688"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/90.993301"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/277467.277477"},{"key":"e_1_3_2_1_24_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_25_1","volume-title":"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_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/645396.651956"},{"key":"e_1_3_2_1_27_1","volume-title":"InphTCP\/IP Illustrated","volume":"1","author":"Wright G. K.","unstructured":"G. K. Wright and W. R. Stevens . TCP state transition diagram . InphTCP\/IP Illustrated , Volume 2: The Implementation http:\/\/www.kohala.com\/start\/pocketguide 1 .ps.]] G. K. Wright and W. R. Stevens. TCP state transition diagram. InphTCP\/IP Illustrated, Volume 2: The Implementation http:\/\/www.kohala.com\/start\/pocketguide1.ps.]]"},{"key":"e_1_3_2_1_28_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.]]"},{"key":"e_1_3_2_1_29_1","first-page":"217","volume-title":"Proc. ICALP","author":"Yi W.","year":"1991","unstructured":"W. Yi . CCS + time = an interleaving model for real time systems . In Proc. ICALP , pages 217 -- 228 , 1991 .]] W. Yi. CCS + time = an interleaving model for real time systems. In Proc. ICALP, pages 217--228, 1991.]]"}],"event":{"name":"POPL06: The 33rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages 2006","location":"Charleston South Carolina USA","acronym":"POPL06","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1111037.1111043","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1111037.1111043","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T17:38:28Z","timestamp":1750268308000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1111037.1111043"}},"subtitle":["HOL specification and symbolic-evaluation testing for TCP implementations"],"short-title":[],"issued":{"date-parts":[[2006,1,11]]},"references-count":26,"alternative-id":["10.1145\/1111037.1111043","10.1145\/1111037"],"URL":"https:\/\/doi.org\/10.1145\/1111037.1111043","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1111320.1111043","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2006,1,11]]},"assertion":[{"value":"2006-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}