{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T00:54:22Z","timestamp":1782953662270,"version":"3.54.5"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031866944","type":"print"},{"value":"9783031866951","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-86695-1_5","type":"book-chapter","created":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T02:06:44Z","timestamp":1746151604000},"page":"70-83","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Proof-Producing Symbolic Execution for\u00a0P4"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9921-3257","authenticated-orcid":false,"given":"Didrik","family":"Lundberg","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8069-6495","authenticated-orcid":false,"given":"Roberto","family":"Guanciale","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5432-6442","authenticated-orcid":false,"given":"Mads","family":"Dam","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,5,3]]},"reference":[{"issue":"OOPSLA1","key":"5_CR1","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1145\/3649819","volume":"8","author":"A Alshnakat","year":"2024","unstructured":"Alshnakat, A., Lundberg, D., Guanciale, R., Dam, M.: HOL4P4: mechanized small-step semantics for P4. Proc. ACM Program. Lang. 8(OOPSLA1), 223\u2013249 (2024). https:\/\/doi.org\/10.1145\/3649819","journal-title":"Proc. ACM Program. Lang."},{"key":"5_CR2","doi-asserted-by":"publisher","unstructured":"Barras, B.: Programming and computing in HOL. In: International Conference on Theorem Proving in Higher Order Logics, pp. 17\u201337. Springer (2000). https:\/\/doi.org\/10.1007\/3-540-44659-1_2","DOI":"10.1007\/3-540-44659-1_2"},{"key":"5_CR3","doi-asserted-by":"publisher","unstructured":"Campbell, B., Stark, I.: Extracting behaviour from an executable instruction set model. In: 2016 Formal Methods in Computer-Aided Design (FMCAD), pp. 33\u201340 (2016). https:\/\/doi.org\/10.1109\/FMCAD.2016.7886658","DOI":"10.1109\/FMCAD.2016.7886658"},{"key":"5_CR4","unstructured":"Collavizza, H., Gordon, M.: Integration of theorem-proving and constraint programming for software verification. Ph. D. thesis, Laboratoire I3S (2009)"},{"key":"5_CR5","doi-asserted-by":"publisher","unstructured":"Doenges, R., Kapp\u00e9, T., Sarracino, J., Foster, N., Morrisett, G.: Leapfrog: certified equivalence for protocol parsers. In: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, pp. 950\u2013965. PLDI 2022 (2022). https:\/\/doi.org\/10.1145\/3519939.3523715","DOI":"10.1145\/3519939.3523715"},{"key":"5_CR6","doi-asserted-by":"publisher","unstructured":"Fox, A.: Improved tool support for machine-code decompilation in HOL4. In: 6th International Conference on Interactive Theorem Proving (ITP 2015), pp. 187\u2013202 (2015). https:\/\/doi.org\/10.1007\/978-3-319-22102-1_12","DOI":"10.1007\/978-3-319-22102-1_12"},{"key":"5_CR7","doi-asserted-by":"publisher","unstructured":"Freire, L., Neves, M., Leal, L., Levchenko, K., Schaeffer-Filho, A., Barcellos, M.: Uncovering bugs in P4 programs with assertion-based verification. In: SOSR \u201918, Proceedings of the Symposium on SDN Research (2018). https:\/\/doi.org\/10.1145\/3185467.3185499","DOI":"10.1145\/3185467.3185499"},{"issue":"OOPSLA2","key":"5_CR8","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1145\/3622799","volume":"7","author":"L Gourdin","year":"2023","unstructured":"Gourdin, L., Bonneau, B., Boulm\u00e9, S., Monniaux, D., B\u00e9rard, A.: Formally verifying optimizations with block simulations. Proc. ACM Program. Lang. 7(OOPSLA2), 59\u201388 (2023). https:\/\/doi.org\/10.1145\/3622799","journal-title":"Proc. ACM Program. Lang."},{"key":"5_CR9","doi-asserted-by":"publisher","unstructured":"Hadi\u00a0Salim, J., et al.: Introducing P4TC-a P4 implementation on Linux kernel using traffic control. In: Proceedings of the 6th on European P4 Workshop, pp. 25\u201332 (2023). https:\/\/doi.org\/10.1145\/3630047.3630193","DOI":"10.1145\/3630047.3630193"},{"key":"5_CR10","doi-asserted-by":"publisher","first-page":"139567","DOI":"10.1109\/ACCESS.2020.3012738","volume":"8","author":"F Hauser","year":"2020","unstructured":"Hauser, F., H\u00e4berle, M., Schmidt, M., Menth, M.: P4-IPsec: site-to-site and host-to-site VPN with IPsec in P4-based SDN. IEEE Access 8, 139567\u2013139586 (2020). https:\/\/doi.org\/10.1109\/ACCESS.2020.3012738","journal-title":"IEEE Access"},{"key":"5_CR11","doi-asserted-by":"publisher","unstructured":"Kanabar, H., Fox, A.C., Myreen, M.O.: Taming an authoritative Armv8 ISA specification: L3 validation and CakeML compiler verification. In: 13th International Conference on Interactive Theorem Proving (ITP 2022). Schloss-Dagstuhl-Leibniz Zentrum f\u00fcr Informatik (2022). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2022.20","DOI":"10.4230\/LIPIcs.ITP.2022.20"},{"key":"5_CR12","doi-asserted-by":"publisher","unstructured":"Keller, C.: Tactic program-based testing and bounded verification in Isabelle\/HOL. In: Tests and Proofs: 12th International Conference, TAP 2018, Held as Part of STAF 2018, Toulouse, France, June 27\u201329, 2018, Proceedings 12, pp. 103\u2013119. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-92994-1_6","DOI":"10.1007\/978-3-319-92994-1_6"},{"issue":"7","key":"5_CR13","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (1976). https:\/\/doi.org\/10.1145\/360248.360252","journal-title":"Commun. ACM"},{"key":"5_CR14","unstructured":"Lindner, A., Guanciale, R., Dam, M.: Proof-producing symbolic execution for binary code verification. arXiv preprint arXiv:2304.08848 (2023)"},{"key":"5_CR15","doi-asserted-by":"publisher","unstructured":"Liu, J., et al.: p4v: practical verification for programmable data planes. In: SIGCOMM \u201918, Proceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication, pp. 490\u2013503 (2018). https:\/\/doi.org\/10.1145\/3230543.3230582","DOI":"10.1145\/3230543.3230582"},{"key":"5_CR16","doi-asserted-by":"publisher","unstructured":"Matthews, J., Moore, J.S., Ray, S., Vroon, D.: Verification condition generation via theorem proving. In: Logic for Programming, Artificial Intelligence, and Reasoning: 13th International Conference, LPAR 2006, Phnom Penh, Cambodia, November 13\u201317, 2006. Proceedings 13, pp. 362\u2013376. Springer (2006). https:\/\/doi.org\/10.1007\/11916277_25","DOI":"10.1007\/11916277_25"},{"key":"5_CR17","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: Proceedings of the Symposium on SDN Research, pp.\u00a01\u20137 (2018). https:\/\/doi.org\/10.1145\/3185467.3185497","DOI":"10.1145\/3185467.3185497"},{"key":"5_CR18","doi-asserted-by":"publisher","unstructured":"Peterson, R., et al.: P4Cub: a little language for big routers. In: Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 303\u2013319 (2023). https:\/\/doi.org\/10.1145\/3554345","DOI":"10.1145\/3554345"},{"key":"5_CR19","doi-asserted-by":"publisher","unstructured":"Bockenek, J.A., Verbeek, F., Lammich, P., Ravindran, B.: Formal verification of memory preservation of $$\\times $$86-64 Binaries. In: Romanovsky, A., Troubitsyna, E., Bitsch, F. (eds.) SAFECOMP 2019. LNCS, vol. 11698, pp. 35\u201349. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-26601-1_3","DOI":"10.1007\/978-3-030-26601-1_3"},{"key":"5_CR20","doi-asserted-by":"publisher","unstructured":"Stoenescu, R., Dumitrescu, D., Popovici, M., Negreanu, L., Raiciu, C.: Debugging P4 programs with Vera. In: Proceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication, pp. 518\u2013532 (2018). https:\/\/doi.org\/10.1145\/3230543.3230548","DOI":"10.1145\/3230543.3230548"},{"key":"5_CR21","doi-asserted-by":"publisher","unstructured":"Strother Moore, J.: Symbolic simulation: an ACL2 approach. In: Gopalakrishnan, G., Windley, P. (eds.) FMCAD 1998. LNCS, vol. 1522, pp. 334\u2013350. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/3-540-49519-3_22","DOI":"10.1007\/3-540-49519-3_22"},{"key":"5_CR22","unstructured":"The P4 Language Consortium: $${\\rm P}4_{16}$$ language specification (2023). https:\/\/p4.org\/p4-spec\/docs\/P4-16-v1.2.4.html"},{"key":"5_CR23","unstructured":"Tu, W., Ruffy, F., Budiu, M.: Linux network programming with P4. In: Linux Plumb. Conf (2018)"},{"key":"5_CR24","doi-asserted-by":"publisher","unstructured":"Tuerk, T.: A formalisation of smallfoot in HOL. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 469\u2013484. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_32","DOI":"10.1007\/978-3-642-03359-9_32"},{"key":"5_CR25","doi-asserted-by":"publisher","unstructured":"Tuerk, T.: A separation logic framework for HOL. Tech. rep., University of Cambridge, Computer Laboratory (2011). https:\/\/doi.org\/10.48456\/tr-799","DOI":"10.48456\/tr-799"},{"key":"5_CR26","doi-asserted-by":"publisher","unstructured":"Wang, Q., Pan, M., Wang, S., Doenges, R., Beringer, L., Appel, A.W.: Foundational verification of stateful P4 packet processing. In: 14th International Conference on Interactive Theorem Proving (ITP 2023). Schloss-Dagstuhl-Leibniz Zentrum f\u00fcr Informatik (2023). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2023.32","DOI":"10.4230\/LIPIcs.ITP.2023.32"}],"container-title":["Lecture Notes in Computer Science","Verified Software. Theories, Tools and Experiments"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-86695-1_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T02:06:49Z","timestamp":1746151609000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-86695-1_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031866944","9783031866951"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-86695-1_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"3 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VSTTE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verified Software: Theories, Tools, and Experiments","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 October 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 October 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vstte2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.soundandcomplete.org\/vstte2024.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}