{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:03:12Z","timestamp":1784793792320,"version":"3.55.0"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032325181","type":"print"},{"value":"9783032325198","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T00:00:00Z","timestamp":1784851200000},"content-version":"vor","delay-in-days":204,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    P4 is a domain-specific language for programming protocol-independent packet processors, where packet parsers describe how incoming bit-streams are structured into headers and fields. Building on work by Doenges et al. (2022), we present\n                    <jats:sc>Octopus<\/jats:sc>\n                    , a tool that translates P4 packet parsers into automata and then attempts to (symbolically) check their equivalence.\n                    <jats:sc>Octopus<\/jats:sc>\n                    produces evidence, either in the form of a bisimulation demonstrating equivalence, or a counterexample bit-stream witnessing a behavioral difference between the two parsers. In contrast with earlier work, our tool can check equivalence between non-trivial parsers within minutes, on consumer hardware. We report on the tool\u2019s implementation and evaluate its usability in networking contexts.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-32519-8_11","type":"book-chapter","created":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T07:18:21Z","timestamp":1784791101000},"page":"198-211","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Octopus: Practical Equivalence Checking of\u00a0P4 Packet Parsers"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-9729-4600","authenticated-orcid":false,"given":"Jort","family":"van Leenen","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6068-880X","authenticated-orcid":false,"given":"Tobias","family":"Kapp\u00e9","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,24]]},"reference":[{"key":"11_CR1","doi-asserted-by":"publisher","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: TACAS 2022. LNCS, vol. 13243, pp. 415\u2013442 (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"11_CR2","doi-asserted-by":"publisher","unstructured":"Berde, P., et al.: ONOS: towards an open, distributed SDN OS. In: HotSDN, pp.\u00a01\u20136 (2014). https:\/\/doi.org\/10.1145\/2620728.2620744","DOI":"10.1145\/2620728.2620744"},{"issue":"3","key":"11_CR3","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1145\/2656877.2656890","volume":"44","author":"P Bosshart","year":"2014","unstructured":"Bosshart, P., et al.: P4: programming protocol-independent packet processors. Comput. Commun. Rev. 44(3), 87\u201395 (2014). https:\/\/doi.org\/10.1145\/2656877.2656890","journal-title":"Comput. Commun. Rev."},{"issue":"1\u20134","key":"11_CR4","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/S10817-018-9458-4","volume":"61","author":"L Czajka","year":"2018","unstructured":"Czajka, L., Kaliszyk, C.: Hammer for Coq: automation for dependent type theory. J. Autom. Reason. 61(1\u20134), 423\u2013453 (2018). https:\/\/doi.org\/10.1007\/S10817-018-9458-4","journal-title":"J. Autom. Reason."},{"key":"11_CR5","doi-asserted-by":"publisher","unstructured":"Dang, H.T., et al.: Whippersnapper: a P4 language benchmark suite. In: SOSR, pp. 95\u2013101 (2017). https:\/\/doi.org\/10.1145\/3050220.3050231","DOI":"10.1145\/3050220.3050231"},{"key":"11_CR6","doi-asserted-by":"publisher","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340 (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"11_CR7","doi-asserted-by":"publisher","unstructured":"Doenges, R., et al.: Petr4: formal foundations for P4 data planes. In: POPL, pp. 1\u201332 (2021). https:\/\/doi.org\/10.1145\/3434322","DOI":"10.1145\/3434322"},{"key":"11_CR8","doi-asserted-by":"publisher","unstructured":"Doenges, R., Kapp\u00e9, T., Sarracino, J., Foster, N., Morrisett, G.: Leapfrog: certified equivalence for protocol parsers. In: PLDI, pp. 950\u2013965 (2022). https:\/\/doi.org\/10.1145\/3519939.3523715","DOI":"10.1145\/3519939.3523715"},{"key":"11_CR9","doi-asserted-by":"publisher","unstructured":"Doenges, R., Kapp\u00e9, T., Sarracino, J., Foster, N., Morrisett, G.: Leapfrog: certified equivalence for protocol parsers (2022). https:\/\/doi.org\/10.48550\/arXiv.2205.08762. Full version including proofs","DOI":"10.48550\/arXiv.2205.08762"},{"key":"11_CR10","doi-asserted-by":"publisher","unstructured":"Ekici, B., et al.: SMTCoq: a plug-in for integrating SMT solvers into Coq. In: CAV 2017. LNCS, vol. 10427, pp. 126\u2013133 (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_7","DOI":"10.1007\/978-3-319-63390-9_7"},{"key":"11_CR11","unstructured":"Gario, M., Micheli, A.: PySMT: a solver-agnostic library for fast prototyping of SMT-based algorithms. In: SMT workshop (2015)"},{"key":"11_CR12","doi-asserted-by":"publisher","unstructured":"He, M., Blenk, A., Kellerer, W., Schmid, S.: Toward consistent state management of adaptive programmable networks based on P4. In: NEAT@SIGCOMM, pp. 29\u201335 (2019). https:\/\/doi.org\/10.1145\/3341558.3342202","DOI":"10.1145\/3341558.3342202"},{"key":"11_CR13","doi-asserted-by":"publisher","unstructured":"Kheradmand, A., Rosu, G.: P4K: a formal semantics of P4 and applications (2018). https:\/\/doi.org\/10.48550\/arXiv.1804.01468","DOI":"10.48550\/arXiv.1804.01468"},{"key":"11_CR14","volume-title":"Computer Networking: A Top-Down Approach","author":"JF Kurose","year":"2022","unstructured":"Kurose, J.F., Ross, K.W.: Computer Networking: A Top-Down Approach, 8th edn. Pearson Education Limited, Harlow (2022)","edition":"8"},{"key":"11_CR15","unstructured":"van Leenen, J.: Practical equivalence checking of P4 packet parsers. Thesis Bachelor Informatica, LIACS, Leiden University (2025). https:\/\/theses.liacs.nl\/3410"},{"key":"11_CR16","doi-asserted-by":"publisher","unstructured":"Liu, J., et al.: P4V: practical verification for programmable data planes. In: SIGCOMM, pp. 490\u2013503 (2018). https:\/\/doi.org\/10.1145\/3230543.3230582","DOI":"10.1145\/3230543.3230582"},{"key":"11_CR17","doi-asserted-by":"publisher","unstructured":"Neves, M., Freire, L., Schaeffer-Filho, A., Barcellos, M.: Verification of P4 programs in feasible time using assertions. In: CoNEXT, pp. 73\u201385 (2018). https:\/\/doi.org\/10.1145\/3281411.3281421","DOI":"10.1145\/3281411.3281421"},{"key":"11_CR18","doi-asserted-by":"publisher","unstructured":"N\u00f6tzli, A., Khan, J., Fingerhut, A., Barrett, C., Athanas, P.: p4pktgen: automated test case generation for P4 programs. In: SOSR, pp.\u00a01\u20137 (2018). https:\/\/doi.org\/10.1145\/3185467.3185497","DOI":"10.1145\/3185467.3185497"},{"key":"11_CR19","doi-asserted-by":"publisher","unstructured":"Ramananandro, T., et al.: EverParse: verified secure zero-copy parsers for authenticated message formats. In: USENIX Security, pp. 1465\u20131482 (2019). https:\/\/doi.org\/10.5555\/3361338.3361440","DOI":"10.5555\/3361338.3361440"},{"issue":"6","key":"11_CR20","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1016\/J.JLAP.2010.03.012","volume":"79","author":"G Rosu","year":"2010","unstructured":"Rosu, G., Serbanuta, T.: An overview of the K semantic framework. J. Log. Algebraic Methods Program. 79(6), 397\u2013434 (2010). https:\/\/doi.org\/10.1016\/J.JLAP.2010.03.012","journal-title":"J. Log. Algebraic Methods Program."},{"key":"11_CR21","doi-asserted-by":"publisher","unstructured":"Sangiorgi, D.: Introduction to Bisimulation and Coinduction. Cambridge University Press (2011). https:\/\/doi.org\/10.1017\/CBO9780511777110","DOI":"10.1017\/CBO9780511777110"},{"issue":"3","key":"11_CR22","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1109\/JSYST.2012.2222000","volume":"7","author":"L Sassaman","year":"2013","unstructured":"Sassaman, L., Patterson, M.L., Bratus, S., Locasto, M.E.: Security applications of formal language theory. IEEE Syst. J. 7(3), 489\u2013500 (2013). https:\/\/doi.org\/10.1109\/JSYST.2012.2222000","journal-title":"IEEE Syst. J."},{"key":"11_CR23","doi-asserted-by":"publisher","unstructured":"Stoenescu, R., Dumitrescu, D., Popovici, M., Negreanu, L., Raiciu, C.: Debugging P4 programs with vera. In: SIGCOMM, pp. 518\u2013532 (2018). https:\/\/doi.org\/10.1145\/3230543.3230548","DOI":"10.1145\/3230543.3230548"},{"key":"11_CR24","unstructured":"The P4 language consortium: P4$$_{16}$$ language specification - version 1.2.5 (2024). https:\/\/p4.org\/wp-content\/uploads\/2024\/10\/P4-16-spec-v1.2.5.html"},{"key":"11_CR25","unstructured":"The P4 Language Consortium: P4C\u2014the P4$$_{16}$$ reference compiler (2026). https:\/\/github.com\/p4lang\/p4c"},{"key":"11_CR26","unstructured":"The Rocq development team: The Rocq Prover (2026). https:\/\/rocq-prover.org\/"},{"key":"11_CR27","doi-asserted-by":"publisher","unstructured":"Tian, B., et al.: Aquila: a practically usable verification system for production-scale programmable data planes. In: SIGCOMM, pp. 17\u201332 (2021). https:\/\/doi.org\/10.1145\/3452296.3472937","DOI":"10.1145\/3452296.3472937"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-32519-8_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T07:18:23Z","timestamp":1784791103000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32519-8_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032325181","9783032325198"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32519-8_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"24 July 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","label":"Disclosure of Interests","group":{"name":"EthicsHeading","label":"Ethics"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"38","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.floc26.org\/program","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}