{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,21]],"date-time":"2026-01-21T18:09:14Z","timestamp":1769018954792,"version":"3.49.0"},"reference-count":102,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2018,12,12]],"date-time":"2018-12-12T00:00:00Z","timestamp":1544572800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100008242","name":"NICTA","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100008242","id-type":"DOI","asserted-by":"crossref"}]},{"name":"St Catharine's College Heller Research Fellowship"},{"name":"EC FET-GC project","award":["IST-2001-33234 PEPITO"],"award-info":[{"award-number":["IST-2001-33234 PEPITO"]}]},{"name":"CMI UROP"},{"name":"EPSRC Programme","award":["EP\/K008528\/1"],"award-info":[{"award-number":["EP\/K008528\/1"]}]},{"name":"REMS: Rigorous Engineering for Mainstream Systems"},{"name":"ERC","award":["789108(ELVER)"],"award-info":[{"award-number":["789108(ELVER)"]}]},{"DOI":"10.13039\/501100000266","name":"EPSRC","doi-asserted-by":"crossref","award":["GR\/N24872 and EP\/C510712"],"award-info":[{"award-number":["GR\/N24872 and EP\/C510712"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]},{"name":"EC Thematic Network","award":["IST-2001-38957 APPSEM 2"],"award-info":[{"award-number":["IST-2001-38957 APPSEM 2"]}]},{"name":"EPSRC Leadership Fellowship","award":["EP\/H005633 (Sewell)"],"award-info":[{"award-number":["EP\/H005633 (Sewell)"]}]},{"name":"Royal Society University Research Fellowship"},{"DOI":"10.13039\/501100000923","name":"Australian Research Council","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100000923","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100015539","name":"Australian Government's","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100015539","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2019,2,28]]},"abstract":"<jats:p>Conventional computer engineering relies on test-and-debug development processes, with the behavior of common interfaces described (at best) with prose specification documents. But prose specifications cannot be used in test-and-debug development in any automated way, and prose is a poor medium for expressing complex (and loose) specifications.<\/jats:p>\n          <jats:p>The TCP\/IP protocols and Sockets API are a good example of this: they play a vital role in modern communication and computation, and interoperability between implementations is essential. But what exactly they are is surprisingly obscure: their original development focused on \u201crough consensus and running code,\u201d augmented by prose RFC specifications that do not precisely define what it means for an implementation to be correct. Ultimately, the actual standard is the de facto one of the common implementations, including, for example, the 15\u00a0000 to 20\u00a0000 lines of the BSD implementation\u2014optimized and multithreaded C code, time dependent, with asynchronous event handlers, intertwined with the operating system, and security critical.<\/jats:p>\n          <jats:p>\n            This article reports on work done in the\n            <jats:italic>Netsem<\/jats:italic>\n            project to develop lightweight mathematically rigorous techniques that can be applied to such systems: to specify their behavior precisely (but loosely enough to permit the required implementation variation) and to test whether these specifications and the implementations correspond with specifications that are\n            <jats:italic>executable as test oracles<\/jats:italic>\n            . We developed post hoc specifications of TCP, UDP, and the Sockets API, both of the service that they provide to applications (in terms of TCP bidirectional stream connections) and of the internal operation of the protocol (in terms of TCP segments and UDP datagrams), together with a testable abstraction function relating the two. These specifications are rigorous, detailed, readable, with broad coverage, and rather accurate. Working within a general-purpose proof assistant (HOL4), we developed\n            <jats:italic>language idioms<\/jats:italic>\n            (within higher-order logic) in which to write the specifications: operational semantics with nondeterminism, time, system calls, monadic relational programming, and so forth. We followed an\n            <jats:italic>experimental semantics<\/jats:italic>\n            approach, validating the specifications against several thousand traces captured from three implementations (FreeBSD, Linux, and WinXP). Many differences between these were identified, as were a number of bugs. Validation was done using a special-purpose\n            <jats:italic>symbolic model checker<\/jats:italic>\n            programmed above HOL4.\n          <\/jats:p>\n          <jats:p>Having demonstrated that our logic-based engineering techniques suffice for handling real-world protocols, we argue that similar techniques could be applied to future critical software infrastructure at design time, leading to cleaner designs and (via specification-based testing) more robust and predictable implementations. In cases where specification looseness can be controlled, this should be possible with lightweight techniques, without the need for a general-purpose proof assistant, at relatively little cost.<\/jats:p>","DOI":"10.1145\/3243650","type":"journal-article","created":{"date-parts":[[2018,12,12]],"date-time":"2018-12-12T12:49:32Z","timestamp":1544618972000},"page":"1-77","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["Engineering with Logic"],"prefix":"10.1145","volume":"66","author":[{"given":"Steve","family":"Bishop","sequence":"first","affiliation":[{"name":"University of Cambridge, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthew","family":"Fairbairn","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hannes","family":"Mehnert","sequence":"additional","affiliation":[{"name":"robur.io, Center for the Cultivation of Technology, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Norrish","sequence":"additional","affiliation":[{"name":"Data61, CSIRO and Australian National University, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tom","family":"Ridge","sequence":"additional","affiliation":[{"name":"University of Leicester, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Sewell","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Smith","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Keith","family":"Wansbrough","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2018,12,12]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"\u201cSeven","author":"Alglave Jade","unstructured":"Jade Alglave and Luc Maranget . 2017. A DIY \u201cSeven \u201d tutorial. Retrieved from http:\/\/diy.inria.fr\/doc\/. Jade Alglave and Luc Maranget. 2017. A DIY \u201cSeven\u201d tutorial. Retrieved from http:\/\/diy.inria.fr\/doc\/."},{"key":"e_1_2_1_2_1","unstructured":"Jade Alglave and Luc Maranget. 2017. Simulating memory models with herd7. Retrieved from http:\/\/diy.inria.fr\/doc\/herd.html.  Jade Alglave and Luc Maranget. 2017. Simulating memory models with herd7. Retrieved from http:\/\/diy.inria.fr\/doc\/herd.html."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_2_1_4_1","first-page":"169","article-title":"Verifying network protocol implementations by symbolic refinement checking. In Proceedings of Computer Aided Verification (CAV'11)","volume":"2102","author":"Alur Rajeev","year":"2001","unstructured":"Rajeev Alur and Bow-Yaw Wang . 2001 . Verifying network protocol implementations by symbolic refinement checking. In Proceedings of Computer Aided Verification (CAV'11) , LNCS 2102. 169 -- 181 . Rajeev Alur and Bow-Yaw Wang. 2001. Verifying network protocol implementations by symbolic refinement checking. In Proceedings of Computer Aided Verification (CAV'11), LNCS 2102. 169--181.","journal-title":"LNCS"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/774763.774783"},{"key":"e_1_2_1_6_1","unstructured":"Alasdair Armstrong Thomas Bauereiss Brian Campbell Kathryn Gray Shaked Flur Anthony Fox Gabriel Kerneis Robert Norton-Wright Christopher Pulte Alastair Reid and Peter Sewell. 2017. Sail. Retrieved from http:\/\/www.cl.cam.ac.uk\/ pes20\/sail\/.  Alasdair Armstrong Thomas Bauereiss Brian Campbell Kathryn Gray Shaked Flur Anthony Fox Gabriel Kerneis Robert Norton-Wright Christopher Pulte Alastair Reid and Peter Sewell. 2017. Sail. Retrieved from http:\/\/www.cl.cam.ac.uk\/ pes20\/sail\/."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837637"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103717"},{"key":"e_1_2_1_9_1","unstructured":"Mark Batty Scott Owens Jean Pichon-Pharabod Susmit Sarkar and Peter Sewell. 2012. CppMem: Interactive C\/C++ memory model. Retrieved from http:\/\/svr-pes20-cppmem.cl.cam.ac.uk\/cppmem.  Mark Batty Scott Owens Jean Pichon-Pharabod Susmit Sarkar and Peter Sewell. 2012. CppMem: Interactive C\/C++ memory model. Retrieved from http:\/\/svr-pes20-cppmem.cl.cam.ac.uk\/cppmem."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2015.39"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360221"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2014.14"},{"key":"e_1_2_1_14_1","unstructured":"Karthikeyan Bhargavan C\u00e9dric Fournet Santiago Zanella-B\u00e9uelin Benjamin Beurdouche Antoine Delignat-Lavaud Markulf Kohlweiss Jean-Karim Zinzindohou\u00e9 Nadim Kobeissi Alfredo Pironti and Pierre-Yves Strub. 2017. miTLS. Retrieved from https:\/\/www.mitls.org.  Karthikeyan Bhargavan C\u00e9dric Fournet Santiago Zanella-B\u00e9uelin Benjamin Beurdouche Antoine Delignat-Lavaud Markulf Kohlweiss Jean-Karim Zinzindohou\u00e9 Nadim Kobeissi Alfredo Pironti and Pierre-Yves Strub. 2017. miTLS. Retrieved from https:\/\/www.mitls.org."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/581771.581775"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/190314.190318"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/783106.783122"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/979922.979927"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICNP.2006.320205"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1080091.1080123"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111043"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062353"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2015.10.012"},{"key":"e_1_2_1_26_1","volume-title":"Proceedings of the Annual Conference on USENIX Annual Technical Conference (ATEC\u201904)","author":"Cantrill Bryan M.","unstructured":"Bryan M. Cantrill , Michael W. Shapiro , and Adam H. Leventhal . 2004. Dynamic instrumentation of production systems . In Proceedings of the Annual Conference on USENIX Annual Technical Conference (ATEC\u201904) . USENIX Association, Berkeley, CA, 2--2. Retrieved from http:\/\/dl.acm.org\/citation.cfm?id&equals;1247415.1247417. Bryan M. Cantrill, Michael W. Shapiro, and Adam H. Leventhal. 2004. Dynamic instrumentation of production systems. In Proceedings of the Annual Conference on USENIX Annual Technical Conference (ATEC\u201904). USENIX Association, Berkeley, CA, 2--2. Retrieved from http:\/\/dl.acm.org\/citation.cfm?id&equals;1247415.1247417."},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of the USENIX Annual Technical Conference (USENIX ATC\u201913)","author":"Cardwell Neal","year":"2013","unstructured":"Neal Cardwell , Yuchung Cheng , Lawrence Brakmo , Matt Mathis , Barath Raghavan , Nandita Dukkipati , Hsiao Keng Jerry Chu , Andreas Terzis , and Tom Herbert . 2013 . Packetdrill: Scriptable network stack testing, from sockets to packets . In Proceedings of the USENIX Annual Technical Conference (USENIX ATC\u201913) . 213--218. Retrieved from https:\/\/www.usenix.org\/conference\/atc13\/packetdrill-scriptable-network-stack-testing-sockets-packets. Neal Cardwell, Yuchung Cheng, Lawrence Brakmo, Matt Mathis, Barath Raghavan, Nandita Dukkipati, Hsiao Keng Jerry Chu, Andreas Terzis, and Tom Herbert. 2013. Packetdrill: Scriptable network stack testing, from sockets to packets. In Proceedings of the USENIX Annual Technical Conference (USENIX ATC\u201913). 213--218. Retrieved from https:\/\/www.usenix.org\/conference\/atc13\/packetdrill-scriptable-network-stack-testing-sockets-packets."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/90.649465"},{"key":"e_1_2_1_29_1","first-page":"113","article-title":"Verification and improvement of the sliding window protocol. In Proceedings of TACAS\u201903","volume":"2619","author":"Chkliaev Dmitri","year":"2003","unstructured":"Dmitri Chkliaev , Jozef Hooman , and Erik de Vink . 2003 . Verification and improvement of the sliding window protocol. In Proceedings of TACAS\u201903 , LNCS 2619. 113 -- 127 . Dmitri Chkliaev, Jozef Hooman, and Erik de Vink. 2003. Verification and improvement of the sliding window protocol. In Proceedings of TACAS\u201903, LNCS 2619. 113--127.","journal-title":"LNCS"},{"key":"e_1_2_1_30_1","volume-title":"Proceedings of the 24th Internet Engineering Task Force. 539--544","author":"Clark Dave","year":"1992","unstructured":"Dave Clark . 1992 . A cloudy crystal ball \u2014 Visions of the future . In Proceedings of the 24th Internet Engineering Task Force. 539--544 . Retrieved from http:\/\/www.ietf.org\/proceedings\/24.pdf. Retrieved 2012\/12\/31. Dave Clark. 1992. A cloudy crystal ball \u2014 Visions of the future. In Proceedings of the 24th Internet Engineering Task Force. 539--544. Retrieved from http:\/\/www.ietf.org\/proceedings\/24.pdf. Retrieved 2012\/12\/31."},{"key":"e_1_2_1_31_1","volume-title":"Mike D. Atkinson and Frank K. H. A. Dehne (Eds.)","volume":"41","author":"Compton Michael","year":"2005","unstructured":"Michael Compton . 2005 . Stenning\u2019s protocol implemented in UDP and verified in Isabelle. In CATS (CRPIT) , Mike D. Atkinson and Frank K. H. A. Dehne (Eds.) , Vol. 41 . Australian Computer Society, 21--30. Michael Compton. 2005. Stenning\u2019s protocol implemented in UDP and verified in Isabelle. In CATS (CRPIT), Mike D. Atkinson and Frank K. H. A. Dehne (Eds.), Vol. 41. Australian Computer Society, 21--30."},{"key":"e_1_2_1_32_1","unstructured":"W. Eddy (Ed). 2017. Transmission control protocol specification draft-ietf-tcpm-rfc793bis-11. Retrieved from https:\/\/datatracker.ietf.org\/doc\/draft-ietf-tcpm-rfc793bis\/?include_text&equals;1.  W. Eddy (Ed). 2017. Transmission control protocol specification draft-ietf-tcpm-rfc793bis-11. Retrieved from https:\/\/datatracker.ietf.org\/doc\/draft-ietf-tcpm-rfc793bis\/?include_text&equals;1."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103719"},{"key":"e_1_2_1_34_1","unstructured":"Christopher Dearlove Joe Touch John C. Klensin Heasley Yoav Nir Petr\u0160pa\u010dek John C Klensin Yoav Nir Eric Rescorla Paul Wouters Carsten Bormann Jaap Akkerhuis Randy Bush John Wroclawski Paul Wouters Brian E. Carpenter Julian Reschke Mark Andrews Christian Huitema Bob Hinden Joel M. Halpern and Dave Cridland. 2017. I-D Action: draft-thomson-postel-was-wrong-01.txt (mailing list thread). Retrieved from https:\/\/mailarchive.ietf.org\/arch\/search\/?email_list&equals;ietf&q&equals;&equals;&equals;postel+was+wrong.  Christopher Dearlove Joe Touch John C. Klensin Heasley Yoav Nir Petr\u0160pa\u010dek John C Klensin Yoav Nir Eric Rescorla Paul Wouters Carsten Bormann Jaap Akkerhuis Randy Bush John Wroclawski Paul Wouters Brian E. Carpenter Julian Reschke Mark Andrews Christian Huitema Bob Hinden Joel M. Halpern and Dave Cridland. 2017. I-D Action: draft-thomson-postel-was-wrong-01.txt (mailing list thread). Retrieved from https:\/\/mailarchive.ietf.org\/arch\/search\/?email_list&equals;ietf&q&equals;&equals;&equals;postel+was+wrong."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/645880.672086"},{"key":"e_1_2_1_36_1","unstructured":"Shaked Flur Jon French Kathyrn E. Gray Christopher Pulte Susmit Sarkar Peter Sewell and Robert Norton-Wright. 2017. rmem. Retrieved from http:\/\/www.cl.cam.ac.uk\/ pes20\/rmem\/.  Shaked Flur Jon French Kathyrn E. Gray Christopher Pulte Susmit Sarkar Peter Sewell and Robert Norton-Wright. 2017. rmem. Retrieved from http:\/\/www.cl.cam.ac.uk\/ pes20\/rmem\/."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837615"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009839"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32347-8_23"},{"key":"e_1_2_1_40_1","unstructured":"FreeBSD TCP testsuite on GitHub. 2016. FreeBSD packetdrill TCP testsuite GitHub repository. Retrieved from https:\/\/github.com\/freebsd-net\/tcp-testsuite.  FreeBSD TCP testsuite on GitHub. 2016. FreeBSD packetdrill TCP testsuite GitHub repository. Retrieved from https:\/\/github.com\/freebsd-net\/tcp-testsuite."},{"key":"e_1_2_1_41_1","unstructured":"Fyodor. {n.d.}. nmap. Retrieved from http:\/\/www.insecure.org\/nmap\/.  Fyodor. {n.d.}. nmap. Retrieved from http:\/\/www.insecure.org\/nmap\/."},{"key":"e_1_2_1_42_1","unstructured":"Galois. 2017. The HaNS package. Retrieved from https:\/\/hackage.haskell.org\/package\/hans https:\/\/github.com\/GaloisInc\/HaNS.  Galois. 2017. The HaNS package. Retrieved from https:\/\/hackage.haskell.org\/package\/hans https:\/\/github.com\/GaloisInc\/HaNS."},{"key":"e_1_2_1_43_1","volume-title":"Wadsworth","author":"Gordon Michael","year":"1979","unstructured":"Michael Gordon , Robin Milner , and Christopher P . Wadsworth . 1979 . Edinburgh LCF , LNCS 78. Michael Gordon, Robin Milner, and Christopher P. Wadsworth. 1979. Edinburgh LCF, LNCS 78."},{"key":"e_1_2_1_44_1","volume-title":"HOL: A Theorem Proving Environment","author":"Gordon M. J. C.","year":"1993","unstructured":"M. J. C. Gordon and T. Melham (Eds.). 1993 . Introduction to HOL: A Theorem Proving Environment . Cambridge University Press . M. J. C. Gordon and T. Melham (Eds.). 1993. Introduction to HOL: A Theorem Proving Environment. Cambridge University Press."},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2830772.2830775"},{"key":"e_1_2_1_46_1","first-page":"119","article-title":"Specifications and proofs for ensemble layers. In Proceedings of TACAS","volume":"1579","author":"Hickey Jason","year":"1999","unstructured":"Jason Hickey , Nancy A. Lynch , and Robbert van Renesse . 1999 . Specifications and proofs for ensemble layers. In Proceedings of TACAS , LNCS 1579. 119 -- 133 . Jason Hickey, Nancy A. Lynch, and Robbert van Renesse. 1999. Specifications and proofs for ensemble layers. In Proceedings of TACAS, LNCS 1579. 119--133.","journal-title":"LNCS"},{"key":"e_1_2_1_47_1","volume-title":"Proceedings of the 8th Euromicro Workshop on Parallel and Distributed Processing.","author":"Hofmann Richard","year":"2000","unstructured":"Richard Hofmann and Frank Lemmen . 2000 . Specification-driven monitoring of TCP\/IP . In Proceedings of the 8th Euromicro Workshop on Parallel and Distributed Processing. Richard Hofmann and Frank Lemmen. 2000. Specification-driven monitoring of TCP\/IP. In Proceedings of the 8th Euromicro Workshop on Parallel and Distributed Processing."},{"key":"e_1_2_1_48_1","unstructured":"HOL 2005. The HOL 4 System Kananaskis-3 release. Retrieved from hol.sourceforge.net.  HOL 2005. The HOL 4 System Kananaskis-3 release. Retrieved from hol.sourceforge.net."},{"key":"e_1_2_1_49_1","volume-title":"P1003.1g","author":"IEEE.","unstructured":"IEEE. 2000. Information Technology\u2014Portable Operating System Interface (POSIX)\u2014Part xx: Protocol Independent Interfaces (PII) , P1003.1g . Institute of Electrical and Electronics Engineers. IEEE. 2000. Information Technology\u2014Portable Operating System Interface (POSIX)\u2014Part xx: Protocol Independent Interfaces (PII), P1003.1g. Institute of Electrical and Electronics Engineers."},{"key":"e_1_2_1_50_1","unstructured":"IXIA. 2005. IxANVL(TM) \u2014 Automated Network Validation Library. Retrieved from http:\/\/www.ixiacom.com\/.  IXIA. 2005. IxANVL(TM) \u2014 Automated Network Validation Library. Retrieved from http:\/\/www.ixiacom.com\/."},{"key":"e_1_2_1_51_1","unstructured":"David Kaloper-Mer\u0161injak and Hannes Mehnert. 2016. Not-quite-so-broken TLS 1.3 mechanised conformance checking. In TLSv1.3 -- Ready or Not? (TRON) Workshop.  David Kaloper-Mer\u0161injak and Hannes Mehnert. 2016. Not-quite-so-broken TLS 1.3 mechanised conformance checking. In TLSv1.3 -- Ready or Not? (TRON) Workshop."},{"key":"e_1_2_1_52_1","volume-title":"24th USENIX Security Symposium (UNISEX Security\u201915)","author":"Kaloper-Mer\u0161injak David","year":"2015","unstructured":"David Kaloper-Mer\u0161injak , Hannes Mehnert , Anil Madhavapeddy , and Peter Sewell . 2015 . Not-quite-so-broken TLS: Lessons in re-engineering a security protocol specification and implementation . In 24th USENIX Security Symposium (UNISEX Security\u201915) . 223--238. Retrieved from https:\/\/www.usenix.org\/conference\/usenixsecurity15\/technical-sessions\/presentation\/kaloper-mersinjak. David Kaloper-Mer\u0161injak, Hannes Mehnert, Anil Madhavapeddy, and Peter Sewell. 2015. Not-quite-so-broken TLS: Lessons in re-engineering a security protocol specification and implementation. In 24th USENIX Security Symposium (UNISEX Security\u201915). 223--238. Retrieved from https:\/\/www.usenix.org\/conference\/usenixsecurity15\/technical-sessions\/presentation\/kaloper-mersinjak."},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2983996"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159913.1159918"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/316188.316200"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004854"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.5555\/645532.656332"},{"key":"e_1_2_1_60_1","first-page":"08","article-title":"The Objective-Caml System","volume":"3","author":"Leroy Xavier","year":"2004","unstructured":"Xavier Leroy , Damien Doligez , Alain Frisch , Jacques Garrigue , Didier R\u00e9my , and J\u00e9r\u00f4me Vouillon . 2004 . The Objective-Caml System , Release 3 . 08 .2. INRIA. Retrieved from http:\/\/caml.inria.fr\/. Xavier Leroy, Damien Doligez, Alain Frisch, Jacques Garrigue, Didier R\u00e9my, and J\u00e9r\u00f4me Vouillon. 2004. The Objective-Caml System, Release 3.08.2. INRIA. Retrieved from http:\/\/caml.inria.fr\/.","journal-title":"Release"},{"key":"e_1_2_1_62_1","unstructured":"Peng Li and Stephan Zdancewic. {n.d.}. Retrieved from http:\/\/www.cl.cam.ac.uk\/&sim;pes20\/Netsem\/unify_with_tcp.tgz.  Peng Li and Stephan Zdancewic. {n.d.}. Retrieved from http:\/\/www.cl.cam.ac.uk\/&sim;pes20\/Netsem\/unify_with_tcp.tgz."},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250756"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0060"},{"key":"e_1_2_1_65_1","unstructured":"m3lt. 1997. The LAND attack (IP DOS). Retrieved from http:\/\/insecure.org\/sploits\/land.ip.DOS.html.  m3lt. 1997. The LAND attack (IP DOS). Retrieved from http:\/\/insecure.org\/sploits\/land.ip.DOS.html."},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89330-1_22"},{"key":"e_1_2_1_67_1","volume-title":"Counterexamples and proof loophole for the C\/C++ to POWER and ARMv7 trailing-sync compiler mappings. CoRR abs\/1611.01507","author":"Manerkar Yatin A.","year":"2016","unstructured":"Yatin A. Manerkar , Caroline Trippel , Daniel Lustig , Michael Pellauer , and Margaret Martonosi . 2016. Counterexamples and proof loophole for the C\/C++ to POWER and ARMv7 trailing-sync compiler mappings. CoRR abs\/1611.01507 ( 2016 ). arxiv:1611.01507. Retrieved from http:\/\/arxiv.org\/abs\/1611.01507. Yatin A. Manerkar, Caroline Trippel, Daniel Lustig, Michael Pellauer, and Margaret Martonosi. 2016. Counterexamples and proof loophole for the C\/C++ to POWER and ARMv7 trailing-sync compiler mappings. CoRR abs\/1611.01507 (2016). arxiv:1611.01507. Retrieved from http:\/\/arxiv.org\/abs\/1611.01507."},{"key":"e_1_2_1_68_1","volume-title":"Watson","author":"McKusick Marshall Kirk","year":"2014","unstructured":"Marshall Kirk McKusick , George Neville-Neil , and Robert N. M . Watson . 2014 . The Design and Implementation of the FreeBSD Operating System (2nd ed.). Addison-Wesley Professional . Marshall Kirk McKusick, George Neville-Neil, and Robert N. M. Watson. 2014. The Design and Implementation of the FreeBSD Operating System (2nd ed.). Addison-Wesley Professional."},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908081"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2491967"},{"key":"e_1_2_1_71_1","volume-title":"2nd Workshop on Compiler Support for System Software. 25--35","author":"Morrisett Greg","year":"1999","unstructured":"Greg Morrisett , Karl Crary , Neal Glew , Dan Grossman , Richard Samuels , Frederick Smith , David Walker , Stephanie Weirich , and Steve Zdancewic . 1999 . TALx86: A realistic typed assembly language . In 2nd Workshop on Compiler Support for System Software. 25--35 . Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick Smith, David Walker, Stephanie Weirich, and Steve Zdancewic. 1999. TALx86: A realistic typed assembly language. In 2nd Workshop on Compiler Support for System Software. 25--35."},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/55482.55495"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/52324.52334"},{"key":"e_1_2_1_74_1","volume-title":"Proceedings of1st Symposium on Networked Systems Design and Implementation (NSDI\u201904)","author":"Musavathi Madanlal","unstructured":"Madanlal Musavathi and Dawson R. Engler . 2004. Model checking large network protocol implementations . In Proceedings of1st Symposium on Networked Systems Design and Implementation (NSDI\u201904) . 155--168. Madanlal Musavathi and Dawson R. Engler. 2004. Model checking large network protocol implementations. In Proceedings of1st Symposium on Networked Systems Design and Implementation (NSDI\u201904). 155--168."},{"key":"e_1_2_1_75_1","unstructured":"Netsem github. 2015. Netsem GitHub repository. Retrieved from https:\/\/github.com\/rems-project\/netsem.  Netsem github. 2015. Netsem GitHub repository. Retrieved from https:\/\/github.com\/rems-project\/netsem."},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133373.1133383"},{"key":"e_1_2_1_79_1","volume-title":"Proceedings of SIGCOMM\u201901","author":"Padhye Jitendra","year":"2001","unstructured":"Jitendra Padhye and Sally Floyd . 2001 . On inferring TCP behaviour . In Proceedings of SIGCOMM\u201901 . Jitendra Padhye and Sally Floyd. 2001. On inferring TCP behaviour. In Proceedings of SIGCOMM\u201901."},{"key":"e_1_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596600.1596612"},{"key":"e_1_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1145\/1088361.1088372"},{"key":"e_1_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.17487\/RFC2398"},{"key":"e_1_2_1_84_1","doi-asserted-by":"publisher","DOI":"10.1145\/263105.263160"},{"key":"e_1_2_1_85_1","volume-title":"A Graph Model Analysis of Computer Communications Protocols","author":"Postel J.","unstructured":"J. Postel . 1974. A Graph Model Analysis of Computer Communications Protocols . University of California, Computer Science Department , PhD Thesis. J. Postel. 1974. A Graph Model Analysis of Computer Communications Protocols. University of California, Computer Science Department, PhD Thesis."},{"key":"e_1_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158107"},{"key":"e_1_2_1_87_1","doi-asserted-by":"crossref","unstructured":"A. Ramaiah R. Stewart and M. Dalal. 2010. RFC 5961: Improving TCP\u2019s Robustness to Blind In-Window Attacks.  A. Ramaiah R. Stewart and M. Dalal. 2010. RFC 5961: Improving TCP\u2019s Robustness to Blind In-Window Attacks.","DOI":"10.17487\/rfc5961"},{"key":"e_1_2_1_88_1","doi-asserted-by":"crossref","unstructured":"Alastair Reid. 2016. Trustworthy specifications of ARM\u00ae v8-A and v8-M system level architecture. In 2016 Formal Methods in Computer-Aided Design (FMCAD\u201916). 161--168.   Alastair Reid. 2016. Trustworthy specifications of ARM\u00ae v8-A and v8-M system level architecture. In 2016 Formal Methods in Computer-Aided Design (FMCAD\u201916). 161--168.","DOI":"10.1109\/FMCAD.2016.7886675"},{"key":"e_1_2_1_89_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480934"},{"key":"e_1_2_1_90_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_21"},{"key":"e_1_2_1_92_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815411"},{"key":"e_1_2_1_93_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254102"},{"key":"e_1_2_1_94_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993520"},{"key":"e_1_2_1_95_1","volume-title":"Proceedings of the International Workshop on Applied Formal Methods in System Design (COST\u201996)","author":"Schieferdecker I.","year":"1996","unstructured":"I. Schieferdecker . 1996 . Abruptly-terminated connections in TCP -- A verification example . In Proceedings of the International Workshop on Applied Formal Methods in System Design (COST\u201996) . I. Schieferdecker. 1996. Abruptly-terminated connections in TCP -- A verification example. In Proceedings of the International Workshop on Applied Formal Methods in System Design (COST\u201996)."},{"key":"e_1_2_1_97_1","doi-asserted-by":"publisher","DOI":"10.5555\/645870.668688"},{"key":"e_1_2_1_98_1","doi-asserted-by":"publisher","DOI":"10.1145\/1785414.1785443"},{"key":"e_1_2_1_99_1","doi-asserted-by":"publisher","DOI":"10.1109\/90.993301"},{"key":"e_1_2_1_100_1","doi-asserted-by":"crossref","unstructured":"M. A. S. Smith. 1996. Formal verification of communication protocols. In Proceedings of Formal Description Techniques IX: Theory Application and Tools IFIP TC6 WG6.1 International Conference on Formal Description Techniques IX \/ Protocol Specification Testing and Verification XVI (FORTE\u201996). 129--144.   M. A. S. Smith. 1996. Formal verification of communication protocols. In Proceedings of Formal Description Techniques IX: Theory Application and Tools IFIP TC6 WG6.1 International Conference on Formal Description Techniques IX \/ Protocol Specification Testing and Verification XVI (FORTE\u201996). 129--144.","DOI":"10.1007\/978-0-387-35079-0_8"},{"key":"e_1_2_1_101_1","volume-title":"1: The Protocols","author":"Stevens W. R.","unstructured":"W. R. Stevens . 1994. TCP\/ IP Illustrated Vol . 1: The Protocols . Addison Wesley . W. R. Stevens. 1994. TCP\/IP Illustrated Vol. 1: The Protocols. Addison Wesley."},{"key":"e_1_2_1_102_1","volume-title":"Networking APIs: Sockets and XTI","author":"Stevens W. Richard","unstructured":"W. Richard Stevens . 1998. UNIX Network Programming Vol. 1 : Networking APIs: Sockets and XTI ( 2 nd ed.). Prentice Hall . W. Richard Stevens. 1998. UNIX Network Programming Vol. 1: Networking APIs: Sockets and XTI (2nd ed.). Prentice Hall.","edition":"2"},{"key":"e_1_2_1_103_1","unstructured":"The Netsem Project. {n.d.}. Web page. Retrieved from http:\/\/www.cl.cam.ac.uk\/users\/pes20\/Netsem\/.  The Netsem Project. {n.d.}. Web page. Retrieved from http:\/\/www.cl.cam.ac.uk\/users\/pes20\/Netsem\/."},{"key":"e_1_2_1_104_1","unstructured":"M. Thomson. 2017. The Harmful Consequences of Postel\u2019s Maxim draft-thomson-postel-was-wrong-01. Retrieved from https:\/\/tools.ietf.org\/html\/draft-thomson-postel-was-wrong-01.  M. Thomson. 2017. The Harmful Consequences of Postel\u2019s Maxim draft-thomson-postel-was-wrong-01. Retrieved from https:\/\/tools.ietf.org\/html\/draft-thomson-postel-was-wrong-01."},{"key":"e_1_2_1_105_1","doi-asserted-by":"publisher","DOI":"10.1007\/11562436_12"},{"key":"e_1_2_1_106_1","first-page":"278","article-title":"Timing UDP: Mechanized semantics for sockets, threads and failures. In Proceedings of ESOP","volume":"2305","author":"Wansbrough Keith","year":"2002","unstructured":"Keith Wansbrough , Michael Norrish , Peter Sewell , and Andrei Serjantov . 2002 . Timing UDP: Mechanized semantics for sockets, threads and failures. In Proceedings of ESOP , LNCS 2305. 278 -- 294 . Keith Wansbrough, Michael Norrish, Peter Sewell, and Andrei Serjantov. 2002. Timing UDP: Mechanized semantics for sockets, threads and failures. In Proceedings of ESOP, LNCS 2305. 278--294.","journal-title":"LNCS"},{"key":"e_1_2_1_107_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009838"},{"key":"e_1_2_1_108_1","doi-asserted-by":"publisher","DOI":"10.5555\/2665671.2665740"},{"key":"e_1_2_1_109_1","volume-title":"2: The Implementation","author":"Wright Gary R.","unstructured":"Gary R. Wright and W. Richard Stevens . 1995. TCP\/ IP Illustrated Vol . 2: The Implementation . Addison-Wesley . Gary R. Wright and W. Richard Stevens. 1995. TCP\/IP Illustrated Vol. 2: The Implementation. Addison-Wesley."},{"key":"e_1_2_1_110_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"},{"key":"e_1_2_1_111_1","volume-title":"Proceedings of ICALP. 217--228","author":"Yi Wang","year":"1991","unstructured":"Wang Yi . 1991 . CCS + Time &equals; An interleaving model for real time systems . In Proceedings of ICALP. 217--228 . Wang Yi. 1991. CCS + Time &equals; An interleaving model for real time systems. In Proceedings of ICALP. 217--228."}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3243650","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3243650","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:57:32Z","timestamp":1750208252000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3243650"}},"subtitle":["Rigorous Test-Oracle Specification and Validation for TCP\/IP and the Sockets API"],"short-title":[],"issued":{"date-parts":[[2018,12,12]]},"references-count":102,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2019,2,28]]}},"alternative-id":["10.1145\/3243650"],"URL":"https:\/\/doi.org\/10.1145\/3243650","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,12,12]]},"assertion":[{"value":"2017-11-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-12-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}