{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,25]],"date-time":"2025-10-25T14:20:45Z","timestamp":1761402045293,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":38,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,8,19]],"date-time":"2019-08-19T00:00:00Z","timestamp":1566172800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1563393"],"award-info":[{"award-number":["CCF-1563393"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,8,19]]},"DOI":"10.1145\/3341302.3342087","type":"proceedings-article","created":{"date-parts":[[2019,8,14]],"date-time":"2019-08-14T19:32:36Z","timestamp":1565811156000},"page":"227-240","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":39,"title":["Formal specification and testing of QUIC"],"prefix":"10.1145","author":[{"given":"Kenneth L.","family":"McMillan","sequence":"first","affiliation":[{"name":"Microsoft Research"}]},{"given":"Lenore D.","family":"Zuck","sequence":"additional","affiliation":[{"name":"University of Illinois"}]}],"member":"320","published-online":{"date-parts":[[2019,8,19]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040314"},{"volume-title":"Handbook of Satisfiability, Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh (Eds.). Frontiers in Artificial Intelligence and Applications","author":"Barrett Clark W.","key":"e_1_3_2_2_2_1","unstructured":"Clark W. Barrett , Roberto Sebastiani , Sanjit A. Seshia , and Cesare Tinelli . 2009. Satisfiability Modulo Theories . In Handbook of Satisfiability, Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh (Eds.). Frontiers in Artificial Intelligence and Applications , Vol. 185 . IOS Press , 825--885. Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. 2009. Satisfiability Modulo Theories. In Handbook of Satisfiability, Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh (Eds.). Frontiers in Artificial Intelligence and Applications, Vol. 185. IOS Press, 825--885."},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2015.39"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.37"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243650"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/800027.808445"},{"key":"e_1_3_2_2_7_1","volume-title":"Proceedings Third Workshop on Models for Formal Analysis of Real Systems and Sixth International Workshop on Verification and Program Transformation, MARS\/VPT@ETAPS","author":"Bozic Josip","year":"2018","unstructured":"Josip Bozic , Lina Marsso , Radu Mateescu , and Franz Wotawa . 2018. A Formal TLS Handshake Model in LNT . In Proceedings Third Workshop on Models for Formal Analysis of Real Systems and Sixth International Workshop on Verification and Program Transformation, MARS\/VPT@ETAPS 2018 , and Sixth International Workshop on Verification and Program Transformation, Thessaloniki, Greece, 20th April 2018. To be published in EPCT , 1--40. Josip Bozic, Lina Marsso, Radu Mateescu, and Franz Wotawa. 2018. A Formal TLS Handshake Model in LNT. In Proceedings Third Workshop on Models for Formal Analysis of Real Systems and Sixth International Workshop on Verification and Program Transformation, MARS\/VPT@ETAPS 2018, and Sixth International Workshop on Verification and Program Transformation, Thessaloniki, Greece, 20th April 2018. To be published in EPCT, 1--40."},{"key":"e_1_3_2_2_8_1","volume-title":"Engler","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar , Daniel Dunbar , and Dawson R . Engler . 2008 . KLEE : Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In 8th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2008, December 8-10, 2008, San Diego, California, USA, Proceedings. USENIX Association , 209--224. Cristian Cadar, Daniel Dunbar, and Dawson R. Engler. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In 8th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2008, December 8-10, 2008, San Diego, California, USA, Proceedings. USENIX Association, 209--224."},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1866307.1866355"},{"volume-title":"Computer Aided Verification - 30th International Conference Part II","author":"Chudnov Andrey","key":"e_1_3_2_2_10_1","unstructured":"Andrey Chudnov , Nathan Collins , Byron Cook , Joey Dodds , Brian Huffman , Colm MacC\u00e1rthaigh , Stephen Magill , Eric Mertens , Eric Mullen , Serdar Tasiran , Aaron Tomb , and Eddy Westbrook . 2018. Continuous Formal Verification of Amazon s2n . In Computer Aided Verification - 30th International Conference Part II , Vol. 10982 . Springer , 430--446. Andrey Chudnov, Nathan Collins, Byron Cook, Joey Dodds, Brian Huffman, Colm MacC\u00e1rthaigh, Stephen Magill, Eric Mertens, Eric Mullen, Serdar Tasiran, Aaron Tomb, and Eddy Westbrook. 2018. Continuous Formal Verification of Amazon s2n. In Computer Aided Verification - 30th International Conference Part II, Vol. 10982. Springer, 430--446."},{"key":"e_1_3_2_2_11_1","volume-title":"Advanced Functional Programming, 4th International School, AFP","author":"Claessen Koen","year":"2002","unstructured":"Koen Claessen , Colin Runciman , Olaf Chitil , John Hughes , and Malcolm Wallace . 2002. Testing and Tracing Lazy Functional Programs Using QuickCheck and Hat . In Advanced Functional Programming, 4th International School, AFP 2002 , Oxford, UK , August 19-24, 2002, Revised Lectures, Vol. 2638 . Springer , 59--99. Koen Claessen, Colin Runciman, Olaf Chitil, John Hughes, and Malcolm Wallace. 2002. Testing and Tracing Lazy Functional Programs Using QuickCheck and Hat. In Advanced Functional Programming, 4th International School, AFP 2002, Oxford, UK, August 19-24, 2002, Revised Lectures, Vol. 2638. Springer, 59--99."},{"key":"e_1_3_2_2_12_1","unstructured":"The Mitre Corporation. 2014. CVE-2014-0160. https:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2014-0160.  The Mitre Corporation. 2014. CVE-2014-0160. https:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2014-0160."},{"key":"e_1_3_2_2_13_1","unstructured":"The Mitre Corporation. 2014. CVE-2014-3566. https:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2014-3566.  The Mitre Corporation. 2014. CVE-2014-3566. https:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2014-3566."},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134063"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1049\/iet-sen:20080012"},{"volume-title":"QUIC: A UDP-Based Multiplexed and Secure Transport (Version 18). https:\/\/tools.ietf.org\/id\/draft-ietf-quic-transport-18.","year":"2019","key":"e_1_3_2_2_17_1","unstructured":"Internet-Draft. 2019 . QUIC: A UDP-Based Multiplexed and Secure Transport (Version 18). https:\/\/tools.ietf.org\/id\/draft-ietf-quic-transport-18. Internet-Draft. 2019. QUIC: A UDP-Based Multiplexed and Secure Transport (Version 18). https:\/\/tools.ietf.org\/id\/draft-ietf-quic-transport-18."},{"volume-title":"QUIC: QUIC Loss Detection and Congestion Control. https:\/\/tools.ietf.org\/html\/draft-ietf-quic-recovery-18.","year":"2019","key":"e_1_3_2_2_18_1","unstructured":"Internet-Draft. 2019 . QUIC: QUIC Loss Detection and Congestion Control. https:\/\/tools.ietf.org\/html\/draft-ietf-quic-recovery-18. Internet-Draft. 2019. QUIC: QUIC Loss Detection and Congestion Control. https:\/\/tools.ietf.org\/html\/draft-ietf-quic-recovery-18."},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2006.05.004"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2714565"},{"key":"e_1_3_2_2_21_1","volume-title":"FMCAD 2016","author":"McMillan Kenneth L.","year":"2016","unstructured":"Kenneth L. McMillan . 2016 . Modular specification and verification of a cache-coherent interface. In 2016 Formal Methods in Computer-Aided Design , FMCAD 2016 , Mountain View, CA, USA , October 3-6, 2016. IEEE, 109--116. Kenneth L. McMillan. 2016. Modular specification and verification of a cache-coherent interface. In 2016 Formal Methods in Computer-Aided Design, FMCAD 2016, Mountain View, CA, USA, October 3-6, 2016. IEEE, 109--116."},{"key":"e_1_3_2_2_22_1","unstructured":"Kenneth L. McMillan. 2019. Mechanized Specification of QUIC. https:\/\/github.com\/microsoft\/ivy\/tree\/master\/doc\/examples\/quic.  Kenneth L. McMillan. 2019. Mechanized Specification of QUIC. https:\/\/github.com\/microsoft\/ivy\/tree\/master\/doc\/examples\/quic."},{"key":"e_1_3_2_2_23_1","volume-title":"Last updated","author":"McMillan Kenneth L.","year":"2019","unstructured":"Kenneth L. McMillan . Last updated 2019 . Ivy . http:\/\/microsoft.github.io\/ivy. Kenneth L. McMillan. Last updated 2019. Ivy. http:\/\/microsoft.github.io\/ivy."},{"key":"e_1_3_2_2_24_1","volume-title":"IEEE Secure Development Conference (SecDev","author":"McMillan K. L.","year":"2019","unstructured":"K. L. McMillan and L. D. Zuck . 2019. Compositional Testing of Network Protocols. http:\/\/mcmil.net\/pubs\/SECDEV19.pdf . In IEEE Secure Development Conference (SecDev 2019 ). To appear. K. L. McMillan and L. D. Zuck. 2019. Compositional Testing of Network Protocols. http:\/\/mcmil.net\/pubs\/SECDEV19.pdf. In IEEE Secure Development Conference (SecDev 2019). To appear."},{"key":"e_1_3_2_2_25_1","volume-title":"FMCAD 2017","author":"Mudduluru Rashmi","year":"2017","unstructured":"Rashmi Mudduluru , Pantazis Deligiannis , Ankush Desai , Akash Lal , and Shaz Qadeer . 2017 . Lasso detection using partial-state caching. In 2017 Formal Methods in Computer Aided Design , FMCAD 2017 , Vienna, Austria , October 2-6, 2017. 84--91. Rashmi Mudduluru, Pantazis Deligiannis, Ankush Desai, Akash Lal, and Shaz Qadeer. 2017. Lasso detection using partial-state caching. In 2017 Formal Methods in Computer Aided Design, FMCAD 2017, Vienna, Austria, October 2-6, 2017. 84--91."},{"key":"e_1_3_2_2_26_1","first-page":"175","article-title":"Protocol Conformance Testing - A Survey. In Computer Networks, Architecture and Applications, S. V. Raghavan et al. (Ed.). Springer","volume":"1","author":"Neelakantan B.","year":"1995","unstructured":"B. Neelakantan and S. V. Raghavan . 1995 . Protocol Conformance Testing - A Survey. In Computer Networks, Architecture and Applications, S. V. Raghavan et al. (Ed.). Springer , Chapter 1 , 175 -- 191 . B. Neelakantan and S. V.Raghavan. 1995. Protocol Conformance Testing - A Survey. In Computer Networks, Architecture and Applications, S. V. Raghavan et al. (Ed.). Springer, Chapter 1, 175--191.","journal-title":"Chapter"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908118"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596600.1596612"},{"key":"e_1_3_2_2_29_1","volume-title":"Analyzing Protocol Implementations for Interoperability. In 12th USENIX Symposium on Networked Systems Design and Implementation, NSDI 15","author":"Pedrosa Luis","year":"2015","unstructured":"Luis Pedrosa , Ari Fogel , Nupur Kothari , Ramesh Govindan , Ratul Mahajan , and Todd D. Millstein . 2015 . Analyzing Protocol Implementations for Interoperability. In 12th USENIX Symposium on Networked Systems Design and Implementation, NSDI 15 , Oakland, CA, USA , May 4-6, 2015 . USENIX Association, 485--498. https:\/\/www.usenix.org\/conference\/nsdi15\/technical-sessions\/presentation\/pedrosa Luis Pedrosa, Ari Fogel, Nupur Kothari, Ramesh Govindan, Ratul Mahajan, and Todd D. Millstein. 2015. Analyzing Protocol Implementations for Interoperability. In 12th USENIX Symposium on Networked Systems Design and Implementation, NSDI 15, Oakland, CA, USA, May 4-6, 2015. USENIX Association, 485--498. https:\/\/www.usenix.org\/conference\/nsdi15\/technical-sessions\/presentation\/pedrosa"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/2867541.2867774"},{"key":"e_1_3_2_2_31_1","volume-title":"State machine inference of QUIC. CoRR abs\/1903.04384","author":"Rasool Abdullah","year":"2019","unstructured":"Abdullah Rasool , Greg Alp\u00e1r , and Joeri de Ruiter . 2019. State machine inference of QUIC. CoRR abs\/1903.04384 ( 2019 ). arXiv:1903.04384 http:\/\/arxiv.org\/abs\/1903.04384 Abdullah Rasool, Greg Alp\u00e1r, and Joeri de Ruiter. 2019. State machine inference of QUIC. CoRR abs\/1903.04384 (2019). arXiv:1903.04384 http:\/\/arxiv.org\/abs\/1903.04384"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3284850.3284853"},{"key":"e_1_3_2_2_33_1","unstructured":"Ivan Ristic. 2014. POODLE Bites TLS. https:\/\/blog.qualys.com\/ssllabs\/2014\/12\/08\/poodle-bites-tls.  Ivan Ristic. 2014. POODLE Bites TLS. https:\/\/blog.qualys.com\/ssllabs\/2014\/12\/08\/poodle-bites-tls."},{"key":"e_1_3_2_2_34_1","unstructured":"Jan R\u00fcth. 2018. How much of the Internet is using QUIC? https:\/\/blog.apnic.net\/2018\/05\/15\/how-much-of-the-internet-is-using-quic\/.  Jan R\u00fcth. 2018. How much of the Internet is using QUIC? https:\/\/blog.apnic.net\/2018\/05\/15\/how-much-of-the-internet-is-using-quic\/."},{"key":"e_1_3_2_2_35_1","series-title":"Lecture Notes in Computer Science","volume-title":"Model-Based Testing of Object-Oriented Reactive Systems with Spec Explorer","author":"Veanes Margus","unstructured":"Margus Veanes , Colin Campbell , Wolfgang Grieskamp , Wolfram Schulte , Nikolai Tillmann , and Lev Nachmanson . 2008. Model-Based Testing of Object-Oriented Reactive Systems with Spec Explorer . Lecture Notes in Computer Science , Vol. 4949 . Springer Verlag , 39--76. Margus Veanes, Colin Campbell, Wolfgang Grieskamp, Wolfram Schulte, Nikolai Tillmann, and Lev Nachmanson. 2008. Model-Based Testing of Object-Oriented Reactive Systems with Spec Explorer. Lecture Notes in Computer Science, Vol. 4949. Springer Verlag, 39--76."},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/0169-7552(90)90132-C"},{"key":"e_1_3_2_2_37_1","unstructured":"QUIC working group. 2019. QUIC Working Group. https:\/\/quicwg.org\/.  QUIC working group. 2019. QUIC Working Group. https:\/\/quicwg.org\/."},{"key":"e_1_3_2_2_38_1","volume-title":"How to Make Chord Correct (Using a Stable Base). CoRR abs\/1502.06461","author":"Zave Pamela","year":"2015","unstructured":"Pamela Zave . 2015. How to Make Chord Correct (Using a Stable Base). CoRR abs\/1502.06461 ( 2015 ). http:\/\/arxiv.org\/abs\/1502.06461 Pamela Zave. 2015. How to Make Chord Correct (Using a Stable Base). CoRR abs\/1502.06461 (2015). http:\/\/arxiv.org\/abs\/1502.06461"}],"event":{"name":"SIGCOMM '19: ACM SIGCOMM 2019 Conference","sponsor":["SIGCOMM ACM Special Interest Group on Data Communication"],"location":"Beijing China","acronym":"SIGCOMM '19"},"container-title":["Proceedings of the ACM Special Interest Group on Data Communication"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341302.3342087","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3341302.3342087","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3341302.3342087","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:12:57Z","timestamp":1750201977000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341302.3342087"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,8,19]]},"references-count":38,"alternative-id":["10.1145\/3341302.3342087","10.1145\/3341302"],"URL":"https:\/\/doi.org\/10.1145\/3341302.3342087","relation":{},"subject":[],"published":{"date-parts":[[2019,8,19]]},"assertion":[{"value":"2019-08-19","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}