{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,17]],"date-time":"2025-10-17T19:58:54Z","timestamp":1760731134206,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":26,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,12,4]],"date-time":"2018-12-04T00:00:00Z","timestamp":1543881600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100010663","name":"H2020 European Research Council","doi-asserted-by":"publisher","award":["647295"],"award-info":[{"award-number":["647295"]}],"id":[{"id":"10.13039\/100010663","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,12,4]]},"DOI":"10.1145\/3284850.3284853","type":"proceedings-article","created":{"date-parts":[[2018,11,28]],"date-time":"2018-11-28T19:16:10Z","timestamp":1543432570000},"page":"15-21","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Interoperability-Guided Testing of QUIC Implementations using Symbolic Execution"],"prefix":"10.1145","author":[{"given":"Felix","family":"Rath","sequence":"first","affiliation":[{"name":"Communication and Distributed Systems, RWTH Aachen University, Aachen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Schemmel","sequence":"additional","affiliation":[{"name":"Communication and Distributed Systems, RWTH Aachen University, Aachen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Klaus","family":"Wehrle","sequence":"additional","affiliation":[{"name":"Communication and Distributed Systems, RWTH Aachen University, Aachen, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2018,12,4]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/11836810_25"},{"volume-title":"Tools and Algorithms for the Construction and Analysis of Systems (Lecture Notes in Computer Science)","author":"Boonstoppel Peter","key":"e_1_3_2_2_2_1","unstructured":"Peter Boonstoppel , Cristian Cadar , and Dawson Engler . 2008. RWset: Attacking Path Explosion in Constraint-Based Test Generation . In Tools and Algorithms for the Construction and Analysis of Systems (Lecture Notes in Computer Science) , C. R. Ramakrishnan and Jakob Rehof (Eds.). Springer Berlin Heidelberg , 351--366. Peter Boonstoppel, Cristian Cadar, and Dawson Engler. 2008. RWset: Attacking Path Explosion in Constraint-Based Test Generation. In Tools and Algorithms for the Construction and Analysis of Systems (Lecture Notes in Computer Science), C. R. Ramakrishnan and Jakob Rehof (Eds.). Springer Berlin Heidelberg, 351--366."},{"key":"e_1_3_2_2_3_1","volume-title":"Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI'08)","volume":"8","author":"Cadar Cristian","unstructured":"Cristian Cadar , Daniel Dunbar , and Dawson R. Engler . 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs .. In Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI'08) , Vol. 8 . 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 Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI'08), Vol. 8. 209--224."},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2408776.2408795"},{"volume-title":"Tools and Algorithms for the Construction and Analysis of Systems (Lecture Notes in Computer Science)","author":"de Moura Leonardo","key":"e_1_3_2_2_5_1","unstructured":"Leonardo de Moura and Nikolaj Bj\u00f8rner . 2008. Z3: An Efficient SMT Solver . In Tools and Algorithms for the Construction and Analysis of Systems (Lecture Notes in Computer Science) , C. R. Ramakrishnan and Jakob Rehof (Eds.). Springer Berlin Heidelberg , 337--340. Leonardo de Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems (Lecture Notes in Computer Science), C. R. Ramakrishnan and Jakob Rehof (Eds.). Springer Berlin Heidelberg, 337--340."},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254088"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2413176.2413207"},{"key":"e_1_3_2_2_8_1","volume-title":"Rajan","author":"Li Guodong","year":"2011","unstructured":"Guodong Li , Indradeep Ghosh , and Sreeranga P . Rajan . 2011 . KLOVER : A Symbolic Execution and Automatic Test Generation Tool for C++ Programs. In Computer Aided Verification (Lecture Notes in Computer Science), Ganesh Gopalakrishnan and Shaz Qadeer (Eds.). Springer Berlin Heidelberg , 609--615. Guodong Li, Indradeep Ghosh, and Sreeranga P. Rajan. 2011. KLOVER: A Symbolic Execution and Automatic Test Generation Tool for C++ Programs. In Computer Aided Verification (Lecture Notes in Computer Science), Ganesh Gopalakrishnan and Shaz Qadeer (Eds.). Springer Berlin Heidelberg, 609--615."},{"key":"e_1_3_2_2_9_1","volume-title":"Jeffrey S. Foster, and Michael Hicks.","author":"Ma Kin-Keung","year":"2011","unstructured":"Kin-Keung Ma , Khoo Yit Phang , Jeffrey S. Foster, and Michael Hicks. 2011 . Directed Symbolic Execution. In Static Analysis (Lecture Notes in Computer Science), Eran Yahav (Ed.). Springer Berlin Heidelberg , 95--111. Kin-Keung Ma, Khoo Yit Phang, Jeffrey S. Foster, and Michael Hicks. 2011. Directed Symbolic Execution. In Static Analysis (Lecture Notes in Computer Science), Eran Yahav (Ed.). Springer Berlin Heidelberg, 95--111."},{"volume-title":"Model Checking Software (Lecture Notes in Computer Science), Dragan Bo\u0161na\u010dki and Stefan Leue (Eds.)","author":"Maggi Paolo","key":"e_1_3_2_2_10_1","unstructured":"Paolo Maggi and Riccardo Sisto . 2002. Using SPIN to Verify Security Properties of Cryptographic Protocols . In Model Checking Software (Lecture Notes in Computer Science), Dragan Bo\u0161na\u010dki and Stefan Leue (Eds.) . Springer Berlin Heidelberg , 187--204. Paolo Maggi and Riccardo Sisto. 2002. Using SPIN to Verify Security Properties of Cryptographic Protocols. In Model Checking Software (Lecture Notes in Computer Science), Dragan Bo\u0161na\u010dki and Stefan Leue (Eds.). Springer Berlin Heidelberg, 187--204."},{"volume-title":"Proceedings of the 7th USENIX Security Symposium (SSYM'98)","author":"Mitchell John C.","key":"e_1_3_2_2_11_1","unstructured":"John C. Mitchell , Vitaly Shmatikov , and Ulrich Stern .1998. Finite-State Analysis of SSL 3.0 . In Proceedings of the 7th USENIX Security Symposium (SSYM'98) . USENIX Association, Berkeley, CA, USA, 16--16. John C. Mitchell, Vitaly Shmatikov, and Ulrich Stern.1998. Finite-State Analysis of SSL 3.0. In Proceedings of the 7th USENIX Security Symposium (SSYM'98). USENIX Association, Berkeley, CA, USA, 16--16."},{"volume-title":"Model Checking Large Network Protocol Implementations. In NSDI '04","author":"Musuvathi Madanlal","key":"e_1_3_2_2_12_1","unstructured":"Madanlal Musuvathi and Dawson R. Engler . 2004 . Model Checking Large Network Protocol Implementations. In NSDI '04 . 155--168. Madanlal Musuvathi and Dawson R. Engler. 2004. Model Checking Large Network Protocol Implementations. In NSDI '04. 155--168."},{"key":"e_1_3_2_2_13_1","volume-title":"Dill","author":"Musuvathi Madanlal","year":"2002","unstructured":"Madanlal Musuvathi , David Y. W. Park , Andy Chou , Dawson R. Engler , and David L . Dill . 2002 . CMC : A Pragmatic Approach to Model Checking Real Code. In Proceedings of the 5th Symposium on Operating Systems Design and implementationCopyright Restrictions Prevent ACM from Being Able to Make the PDFs for This Conference Available for Downloading (OSDI '02). USENIX Association , Berkeley, CA, USA, 75--88. Madanlal Musuvathi, David Y. W. Park, Andy Chou, Dawson R. Engler, and David L. Dill. 2002. CMC: A Pragmatic Approach to Model Checking Real Code. In Proceedings of the 5th Symposium on Operating Systems Design and implementationCopyright Restrictions Prevent ACM from Being Able to Make the PDFs for This Conference Available for Downloading (OSDI '02). USENIX Association, Berkeley, CA, USA, 75--88."},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/2789770.2789804"},{"volume-title":"Proceedings of the 24th USENIX Conference on Security Symposium (SEC'15)","author":"David","key":"e_1_3_2_2_15_1","unstructured":"David A. Ramos and Dawson Engler. 2015. Under-Constrained Symbolic Execution: Correctness Checking for Real Code . In Proceedings of the 24th USENIX Conference on Security Symposium (SEC'15) . USENIX Association, Berkeley, CA, USA, 49--64. David A. Ramos and Dawson Engler. 2015. Under-Constrained Symbolic Execution: Correctness Checking for Real Code. In Proceedings of the 24th USENIX Conference on Security Symposium (SEC'15). USENIX Association, Berkeley, CA, USA, 49--64."},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3123878.3131977"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1791212.1791235"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1460412.1460485"},{"key":"e_1_3_2_2_19_1","volume-title":"Thomas Noll, and Klaus Wehrle.","author":"Schemmel Daniel","year":"2018","unstructured":"Daniel Schemmel , Julian B\u00fcning , Oscar Soria Dustmann , Thomas Noll, and Klaus Wehrle. 2018 . Symbolic Liveness Analysis of Real-World Software. In Computer Aided Verification (Lecture Notes in Computer Science), Hana Chockler and Georg Weissenbacher (Eds.). Springer International Publishing , 447--466. Daniel Schemmel, Julian B\u00fcning, Oscar Soria Dustmann, Thomas Noll, and Klaus Wehrle. 2018. Symbolic Liveness Analysis of Real-World Software. In Computer Aided Verification (Lecture Notes in Computer Science), Hana Chockler and Georg Weissenbacher (Eds.). Springer International Publishing, 447--466."},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2015.23294"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.16602"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2014.2323977"},{"volume-title":"Theoretical and Practical Aspects of SPIN Model Checking (Lecture Notes in Computer Science)","author":"Stahl Karsten","key":"e_1_3_2_2_23_1","unstructured":"Karsten Stahl , Kai Baukus , Yassine Lakhnech , and Martin Stefen . 1999. Divide, Abstract, and Model-Check. In Theoretical and Practical Aspects of SPIN Model Checking (Lecture Notes in Computer Science) , Dennis Dams, Rob Gerth, Stefan Leue, and Mieke Massink (Eds.). Springer Berlin Heidelberg , 57--76. Karsten Stahl, Kai Baukus, Yassine Lakhnech, and Martin Stefen. 1999. Divide, Abstract, and Model-Check. In Theoretical and Practical Aspects of SPIN Model Checking (Lecture Notes in Computer Science), Dennis Dams, Rob Gerth, Stefan Leue, and Mieke Massink (Eds.). Springer Berlin Heidelberg, 57--76."},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2934872.2934881"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3098822.3098833"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSSS.2012.208"}],"event":{"name":"CoNEXT '18: The 14th International Conference on emerging Networking EXperiments and Technologies","sponsor":["SIGCOMM ACM Special Interest Group on Data Communication"],"location":"Heraklion Greece","acronym":"CoNEXT '18"},"container-title":["Proceedings of the Workshop on the Evolution, Performance, and Interoperability of QUIC"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3284850.3284853","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3284850.3284853","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:43:34Z","timestamp":1750207414000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3284850.3284853"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,12,4]]},"references-count":26,"alternative-id":["10.1145\/3284850.3284853","10.1145\/3284850"],"URL":"https:\/\/doi.org\/10.1145\/3284850.3284853","relation":{},"subject":[],"published":{"date-parts":[[2018,12,4]]},"assertion":[{"value":"2018-12-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}