{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,22]],"date-time":"2026-01-22T23:17:55Z","timestamp":1769123875441,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":32,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,8,7]],"date-time":"2018-08-07T00:00:00Z","timestamp":1533600000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100007601","name":"Horizon 2020 Framework Programme","doi-asserted-by":"publisher","award":["671566"],"award-info":[{"award-number":["671566"]}],"id":[{"id":"10.13039\/501100007601","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100010663","name":"European Research Council","doi-asserted-by":"publisher","award":["758815"],"award-info":[{"award-number":["758815"]}],"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,8,7]]},"DOI":"10.1145\/3230543.3230548","type":"proceedings-article","created":{"date-parts":[[2018,8,8]],"date-time":"2018-08-08T19:13:06Z","timestamp":1533755586000},"page":"518-532","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":76,"title":["Debugging P4 programs with vera"],"prefix":"10.1145","author":[{"given":"Radu","family":"Stoenescu","sequence":"first","affiliation":[{"name":"University Politehnica of Bucharest"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dragos","family":"Dumitrescu","sequence":"additional","affiliation":[{"name":"University Politehnica of Bucharest"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matei","family":"Popovici","sequence":"additional","affiliation":[{"name":"University Politehnica of Bucharest"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lorina","family":"Negreanu","sequence":"additional","affiliation":[{"name":"University Politehnica of Bucharest"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Costin","family":"Raiciu","sequence":"additional","affiliation":[{"name":"University Politehnica of Bucharest"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2018,8,7]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3098822.3098834"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2656877.2656890"},{"key":"e_1_3_2_1_3_1","volume-title":"Proc. OSDI'08","author":"Cadar Cristian","unstructured":"Cristian Cadar , Daniel Dunbar , and Dawson Engler . \"KLEE : Unassisted and Automatic Generation of High-coverage Tests for Complex Systems Programs \". In: Proc. OSDI'08 . Cristian Cadar, Daniel Dunbar, and Dawson Engler. \"KLEE: Unassisted and Automatic Generation of High-coverage Tests for Complex Systems Programs\". In: Proc. OSDI'08."},{"key":"e_1_3_2_1_4_1","volume-title":"Proc. NSDI'12","author":"Canini Marco","unstructured":"Marco Canini , Daniele Venzano , Peter Pere\u0161\u00edni , Dejan Kosti\u0107 , and Jennifer Rexford . \" A NICE Way to Test Openflow Applications\". In: Proc. NSDI'12 . Marco Canini, Daniele Venzano, Peter Pere\u0161\u00edni, Dejan Kosti\u0107, and Jennifer Rexford. \"A NICE Way to Test Openflow Applications\". In: Proc. NSDI'12."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1950365.1950396"},{"key":"e_1_3_2_1_6_1","volume-title":"Model Checking","author":"Clarke Edmund M.","year":"1999","unstructured":"Edmund M. Clarke Jr ., Orna Grumberg , and Doron A. Peled . Model Checking . Cambridge, MA, USA : MIT Press , 1999 . isbn: 0-262-03270-8. Edmund M. Clarke Jr., Orna Grumberg, and Doron A. Peled. Model Checking. Cambridge, MA, USA: MIT Press, 1999. isbn: 0-262-03270-8."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2935634.2935638"},{"key":"e_1_3_2_1_8_1","volume-title":"Proc. NSDI'14","author":"Dobrescu Mihai","unstructured":"Mihai Dobrescu and Katerina Argyraki . \" Software Dataplane Verification\". In: Proc. NSDI'14 . NSDI'14. Mihai Dobrescu and Katerina Argyraki. \"Software Dataplane Verification\". In: Proc. NSDI'14. NSDI'14."},{"key":"e_1_3_2_1_9_1","volume-title":"NSDI.","author":"Fogel Ari","year":"2015","unstructured":"Ari Fogel , Stanley Fung , Luis Pedrosa , Meg Walraed-Sullivan , Ramesh Govindan , Ratul Mahajan , and Todd Millstein . \" A General Approach to Network Configuration Analysis\". In: NSDI. 2015 . Ari Fogel, Stanley Fung, Luis Pedrosa, Meg Walraed-Sullivan, Ramesh Govindan, Ratul Mahajan, and Todd Millstein. \"A General Approach to Network Configuration Analysis\". In: NSDI. 2015."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3185467.3185499"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2934872.2934876"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3098822.3098825"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1592681.1592683"},{"key":"e_1_3_2_1_14_1","volume-title":"Proc. NSDI'13","author":"Kazemian Peyman","unstructured":"Peyman Kazemian , Michael Chang , Hongyi Zeng , George Varghese , Nick McKeown , and Scott Whyte . \" Real Time Network Policy Checking Using Header Space Analysis\". In: Proc. NSDI'13 . Peyman Kazemian, Michael Chang, Hongyi Zeng, George Varghese, Nick McKeown, and Scott Whyte. \"Real Time Network Policy Checking Using Header Space Analysis\". In: Proc. NSDI'13."},{"key":"e_1_3_2_1_15_1","volume-title":"Proc. NSDI'12","author":"Kazemian Peyman","unstructured":"Peyman Kazemian , George Varghese , and Nick McKeown . \" Header Space Analysis : Static Checking for Networks \". In: Proc. NSDI'12 . Peyman Kazemian, George Varghese, and Nick McKeown. \"Header Space Analysis: Static Checking for Networks\". In: Proc. NSDI'12."},{"key":"e_1_3_2_1_16_1","volume-title":"Executable Formal Semantics of P4 and Applications","author":"Kheradmand Ali","year":"2017","unstructured":"Ali Kheradmand and Grigore Rosu . Executable Formal Semantics of P4 and Applications . 2017 . Ali Kheradmand and Grigore Rosu. Executable Formal Semantics of P4 and Applications. 2017."},{"key":"e_1_3_2_1_17_1","volume-title":"Proc. NSDI'13","author":"Khurshid Ahmed","unstructured":"Ahmed Khurshid , Xuan Zou , Wenxuan Zhou , Matthew Caesar , and P. Brighten Godfrey . \" VeriFlow: Verifying Network-wide Invariants in Real Time \". In: Proc. NSDI'13 . Ahmed Khurshid, Xuan Zou, Wenxuan Zhou, Matthew Caesar, and P. Brighten Godfrey. \"VeriFlow: Verifying Network-wide Invariants in Real Time\". In: Proc. NSDI'13."},{"key":"e_1_3_2_1_18_1","first-page":"59","volume-title":"Proceedings of the 12th USENIX Conference on Networked Systems Design and Implementation. NSDI'15. Oakland, CA: USENIX Association, 2015","author":"Kim Hyojoon","year":"1971","unstructured":"Hyojoon Kim , Joshua Reich , Arpit Gupta , Muhammad Shahbaz , Nick Feamster , and Russ Clark . \"Kinetic : Verifiable Dynamic Network Control \". In: Proceedings of the 12th USENIX Conference on Networked Systems Design and Implementation. NSDI'15. Oakland, CA: USENIX Association, 2015 , pp. 59 -- 72 . isbn: 978-1-93 1971 -218. url: http:\/\/dl.acm.org\/citation.cfm?id=2789770.2789775. Hyojoon Kim, Joshua Reich, Arpit Gupta, Muhammad Shahbaz, Nick Feamster, and Russ Clark. \"Kinetic: Verifiable Dynamic Network Control\". In: Proceedings of the 12th USENIX Conference on Networked Systems Design and Implementation. NSDI'15. Oakland, CA: USENIX Association, 2015, pp. 59--72. isbn: 978-1-931971-218. url: http:\/\/dl.acm.org\/citation.cfm?id=2789770.2789775."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/354871.354874"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132759"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3230543.3230582"},{"key":"e_1_3_2_1_22_1","volume-title":"Proc. NSDI'15","author":"Lopes Nuno P.","unstructured":"Nuno P. Lopes , Nikolaj Bj\u00f8rner , Patrice Godefroid , Karthick Jayaraman , and George Varghese . \" Checking Beliefs in Dynamic Networks\". In: Proc. NSDI'15 . Nuno P. Lopes, Nikolaj Bj\u00f8rner, Patrice Godefroid, Karthick Jayaraman, and George Varghese. \"Checking Beliefs in Dynamic Networks\". In: Proc. NSDI'15."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2018436.2018470"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/ANCS.2017.33"},{"key":"e_1_3_2_1_25_1","volume-title":"Automatically verifying reachability and well-formedness in P4 Networks. Tech. rep","author":"McKeown Nick","year":"2016","unstructured":"Nick McKeown , Dan Talayco , George Varghese , Nuno Lopes , Nikolaj Bjorner , and Andrey Rybalchenko . Automatically verifying reachability and well-formedness in P4 Networks. Tech. rep . Sept. 2016 . url: https:\/\/www.microsoft.com\/en-us\/research\/publication\/automatically-verifying-reachability-well-formedness-p4-networks\/. Nick McKeown, Dan Talayco, George Varghese, Nuno Lopes, Nikolaj Bjorner, and Andrey Rybalchenko. Automatically verifying reachability and well-formedness in P4 Networks. Tech. rep. Sept. 2016. url: https:\/\/www.microsoft.com\/en-us\/research\/publication\/automatically-verifying-reachability-well-formedness-p4-networks\/."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3185467.3185497"},{"key":"e_1_3_2_1_27_1","volume-title":"15th USENIX Symposium on Networked Systems Design and Implementation (NSDI 18)","author":"Olteanu Vladimir","year":"2018","unstructured":"Vladimir Olteanu , Alexandru Agache , Andrei Voinescu , and Costin Raiciu . \" Stateless Datacenter Load-balancing with Beamer\". In: 15th USENIX Symposium on Networked Systems Design and Implementation (NSDI 18) . Renton, WA: USENIX Association , 2018 . url: https:\/\/www.usenix.org\/conference\/nsdi18\/presentation\/olteanu. Vladimir Olteanu, Alexandru Agache, Andrei Voinescu, and Costin Raiciu. \"Stateless Datacenter Load-balancing with Beamer\". In: 15th USENIX Symposium on Networked Systems Design and Implementation (NSDI 18). Renton, WA: USENIX Association, 2018. url: https:\/\/www.usenix.org\/conference\/nsdi18\/presentation\/olteanu."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491185.2491187"},{"key":"e_1_3_2_1_29_1","first-page":"683","volume-title":"14th USENIX Symposium on Networked Systems Design and Implementation (NSDI 17)","author":"Ryzhyk Leonid","year":"2017","unstructured":"Leonid Ryzhyk , Nikolaj Bj\u00f8rner , Marco Canini , Jean-Baptiste Jeannin , Cole Schlesinger , Douglas B. Terry , and George Varghese . \" Correct by Construction Networks Using Stepwise Refinement\". In: 14th USENIX Symposium on Networked Systems Design and Implementation (NSDI 17) . Boston, MA: USENIX Association , 2017 , pp. 683 -- 698 . isbn: 978-1-931971-37-9. url: https:\/\/www.usenix.org\/conference\/nsdi17\/technical-sessions\/presentation\/ryzhyk. Leonid Ryzhyk, Nikolaj Bj\u00f8rner, Marco Canini, Jean-Baptiste Jeannin, Cole Schlesinger, Douglas B. Terry, and George Varghese. \"Correct by Construction Networks Using Stepwise Refinement\". In: 14th USENIX Symposium on Networked Systems Design and Implementation (NSDI 17). Boston, MA: USENIX Association, 2017, pp. 683--698. isbn: 978-1-931971-37-9. url: https:\/\/www.usenix.org\/conference\/nsdi17\/technical-sessions\/presentation\/ryzhyk."},{"key":"e_1_3_2_1_30_1","volume-title":"Debugging P4 Programs with Vera. Tech. rep","author":"Stoenescu Radu","year":"2018","unstructured":"Radu Stoenescu , Matei Popovici , Lorina Negreanu , and Costin Raiciu . Debugging P4 Programs with Vera. Tech. rep . June 2018 . url: http:\/\/nets.cs.pub.ro\/~costin\/files\/vera-tr.pdf. Radu Stoenescu, Matei Popovici, Lorina Negreanu, and Costin Raiciu. Debugging P4 Programs with Vera. Tech. rep. June 2018. url: http:\/\/nets.cs.pub.ro\/~costin\/files\/vera-tr.pdf."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2934872.2934881"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3098822.3098833"}],"event":{"name":"SIGCOMM '18: ACM SIGCOMM 2018 Conference","location":"Budapest Hungary","acronym":"SIGCOMM '18","sponsor":["SIGCOMM ACM Special Interest Group on Data Communication"]},"container-title":["Proceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3230543.3230548","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3230543.3230548","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:39:23Z","timestamp":1750210763000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3230543.3230548"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,8,7]]},"references-count":32,"alternative-id":["10.1145\/3230543.3230548","10.1145\/3230543"],"URL":"https:\/\/doi.org\/10.1145\/3230543.3230548","relation":{},"subject":[],"published":{"date-parts":[[2018,8,7]]},"assertion":[{"value":"2018-08-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}