{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,24]],"date-time":"2025-08-24T01:21:51Z","timestamp":1755998511437,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":57,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,6,9]],"date-time":"2022-06-09T00:00:00Z","timestamp":1654732800000},"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":[[2022,6,9]]},"DOI":"10.1145\/3519939.3523715","type":"proceedings-article","created":{"date-parts":[[2022,6,2]],"date-time":"2022-06-02T21:05:05Z","timestamp":1654203905000},"page":"950-965","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Leapfrog: certified equivalence for protocol parsers"],"prefix":"10.1145","author":[{"given":"Ryan","family":"Doenges","sequence":"first","affiliation":[{"name":"Cornell University, USA"}]},{"given":"Tobias","family":"Kapp\u00e9","sequence":"additional","affiliation":[{"name":"University of Amsterdam, Netherlands"}]},{"given":"John","family":"Sarracino","sequence":"additional","affiliation":[{"name":"Cornell University, USA"}]},{"given":"Nate","family":"Foster","sequence":"additional","affiliation":[{"name":"Cornell University, USA"}]},{"given":"Greg","family":"Morrisett","sequence":"additional","affiliation":[{"name":"Cornell University, USA"}]}],"member":"320","published-online":{"date-parts":[[2022,6,9]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19718-5_1"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1098\/rsta.2016.0331"},{"volume-title":"Program Logics for Certified Compilers","author":"Appel Andrew W.","key":"e_1_3_2_1_3_1","unstructured":"Andrew W. Appel , Robert Dockins , Aquinas Hobor , Lennart Beringer , Josiah Dodds , Gordon Stewart , Sandrine Blazy , and Xavier Leroy . 2014. Program Logics for Certified Compilers . Cambridge University Press . isbn:978-1-10-704801-0 Andrew W. Appel, Robert Dockins, Aquinas Hobor, Lennart Beringer, Josiah Dodds, Gordon Stewart, Sandrine Blazy, and Xavier Leroy. 2014. Program Logics for Certified Compilers. Cambridge University Press. isbn:978-1-10-704801-0"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25379-9_12"},{"key":"e_1_3_2_1_5_1","unstructured":"Internet Assigned Numbers Authority. 2018. Internet Protocol Version 4 (IPv4) Parameters. https:\/\/www.iana.org\/assignments\/ip-parameters\/ip-parameters.xhtml  Internet Assigned Numbers Authority. 2018. Internet Protocol Version 4 (IPv4) Parameters. https:\/\/www.iana.org\/assignments\/ip-parameters\/ip-parameters.xhtml"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"e_1_3_2_1_7_1","volume-title":"Proc. of the 8th International Workshop on Satisfiability Modulo Theories (SMT","volume":"14","author":"Barrett Clark W.","year":"2010","unstructured":"Clark W. Barrett , Aaron Stump , and Cesare Tinelli . 2010 . The SMT-LIB Standard: Version 2.0 . In Proc. of the 8th International Workshop on Satisfiability Modulo Theories (SMT , Vol. 13). 14\u2013 14 . Clark W. Barrett, Aaron Stump, and Cesare Tinelli. 2010. The SMT-LIB Standard: Version 2.0. In Proc. of the 8th International Workshop on Satisfiability Modulo Theories (SMT, Vol. 13). 14\u201314."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429124"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2656877.2656890"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0023733"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(92)90018-7"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56496-9_9"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314596"},{"issue":"2","key":"e_1_3_2_1_16_1","first-page":"2","article-title":"P4 Language Specification","volume":"1","author":"The P4 Language Consortium","year":"2021","unstructured":"The P4 Language Consortium . 2021 . P4 Language Specification , Version 1 . 2 . 2 . Available at https:\/\/p4.org\/p4-spec\/docs\/P4-16-v1.2.2.html The P4 Language Consortium. 2021. P4 Language Specification, Version 1.2.2. Available at https:\/\/p4.org\/p4-spec\/docs\/P4-16-v1.2.2.html","journal-title":"Version"},{"key":"e_1_3_2_1_17_1","unstructured":"The Coq Development Team. 2021. The Coq Reference Manual version 8.14. Available electronically at http:\/\/coq.inria.fr\/doc  The Coq Development Team. 2021. The Coq Reference Manual version 8.14. Available electronically at http:\/\/coq.inria.fr\/doc"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52148-8_30"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9458-4"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2018.03.017"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35873-9_5"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341686"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71209-1_13"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2579818"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/ANCS.2013.6665172"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60579-7_3"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000010"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00172-F"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-12-417750-5.50022-1"},{"key":"e_1_3_2_1_32_1","volume-title":"Karp","author":"Hopcroft John","year":"1971","unstructured":"John Hopcroft and Richard M . Karp . 1971 . A Linear Algorithm for Testing Equivalence of Finite Automata. Cornell University , Ithaca, NY. https:\/\/hdl.handle.net\/1813\/5958 John Hopcroft and Richard M. Karp. 1971. A Linear Algorithm for Testing Equivalence of Finite Automata. Cornell University, Ithaca, NY. https:\/\/hdl.handle.net\/1813\/5958"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2480359.2429093"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/IEEESTD.2018.8403927"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/800221.806724"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192377"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3230543.3230582"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.4457887"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/36177.36194"},{"volume-title":"Gedanken-Experiments on Sequential Machines","author":"Moore Edward F.","key":"e_1_3_2_1_40_1","unstructured":"Edward F. Moore . 2016. Gedanken-Experiments on Sequential Machines . Princeton University Press , 129\u2013154. https:\/\/doi.org\/doi:10.1515\/9781400882618-006 10.1515\/9781400882618-006 Edward F. Moore. 2016. Gedanken-Experiments on Sequential Machines. Princeton University Press, 129\u2013154. https:\/\/doi.org\/doi:10.1515\/9781400882618-006"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24288-5_19"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349314"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3281411.3281421"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.3233\/sat190101"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1137\/0216062"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.17487\/RFC0768"},{"key":"e_1_3_2_1_47_1","volume-title":"EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats. In 28th USENIX Security Symposium (USENIX Security). 1465\u20131482","author":"Ramananandro Tahina","year":"2019","unstructured":"Tahina Ramananandro , Antoine Delignat-Lavaud , C\u00e9dric Fournet , Nikhil Swamy , Tej Chajed , Nadim Kobeissi , and Jonathan Protzenko . 2019 . EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats. In 28th USENIX Security Symposium (USENIX Security). 1465\u20131482 . isbn:978-1-939133-06-9 https:\/\/www.usenix.org\/conference\/usenixsecurity19\/presentation\/delignat-lavaud Tahina Ramananandro, Antoine Delignat-Lavaud, C\u00e9dric Fournet, Nikhil Swamy, Tej Chajed, Nadim Kobeissi, and Jonathan Protzenko. 2019. EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats. In 28th USENIX Security Symposium (USENIX Security). 1465\u20131482. isbn:978-1-939133-06-9 https:\/\/www.usenix.org\/conference\/usenixsecurity19\/presentation\/delignat-lavaud"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSYST.2012.2222000"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_29"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341690"},{"key":"e_1_3_2_1_51_1","unstructured":"Thomas Streicher. 1993. Investigations into Intensional Type Theory. Habilitiation Thesis Ludwig Maximilian Universit\u00e4t https:\/\/www2.mathematik.tu-darmstadt.de\/~streicher\/HabilStreicher.pdf  Thomas Streicher. 1993. Investigations into Intensional Type Theory. Habilitiation Thesis Ludwig Maximilian Universit\u00e4t https:\/\/www2.mathematik.tu-darmstadt.de\/~streicher\/HabilStreicher.pdf"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3452296.3472937"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542512"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.17487\/RFC3031"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473589"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110269"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373813"}],"event":{"name":"PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"San Diego CA USA","acronym":"PLDI '22"},"container-title":["Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3519939.3523715","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3519939.3523715","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:10:30Z","timestamp":1750183830000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3519939.3523715"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,6,9]]},"references-count":57,"alternative-id":["10.1145\/3519939.3523715","10.1145\/3519939"],"URL":"https:\/\/doi.org\/10.1145\/3519939.3523715","relation":{},"subject":[],"published":{"date-parts":[[2022,6,9]]},"assertion":[{"value":"2022-06-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}