{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,6]],"date-time":"2026-02-06T22:45:17Z","timestamp":1770417917999,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":55,"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"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,8,7]]},"DOI":"10.1145\/3230543.3230582","type":"proceedings-article","created":{"date-parts":[[2018,8,8]],"date-time":"2018-08-08T19:13:06Z","timestamp":1533755586000},"page":"490-503","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":102,"title":["p4v"],"prefix":"10.1145","author":[{"given":"Jed","family":"Liu","sequence":"first","affiliation":[{"name":"Barefoot Networks"}]},{"given":"William","family":"Hallahan","sequence":"additional","affiliation":[{"name":"Yale University"}]},{"given":"Cole","family":"Schlesinger","sequence":"additional","affiliation":[{"name":"Barefoot Networks"}]},{"given":"Milad","family":"Sharif","sequence":"additional","affiliation":[{"name":"Barefoot Networks"}]},{"given":"Jeongkeun","family":"Lee","sequence":"additional","affiliation":[{"name":"Barefoot Networks"}]},{"given":"Robert","family":"Soul\u00e9","sequence":"additional","affiliation":[{"name":"University of Lugano, Lugano, Switzerland"}]},{"given":"Han","family":"Wang","sequence":"additional","affiliation":[{"name":"Barefoot Networks"}]},{"given":"C\u0103lin","family":"Ca\u015fcaval","sequence":"additional","affiliation":[{"name":"Barefoot Networks"}]},{"given":"Nick","family":"McKeown","sequence":"additional","affiliation":[{"name":"Stanford University"}]},{"given":"Nate","family":"Foster","sequence":"additional","affiliation":[{"name":"Cornell University"}]}],"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\/2535838.2535862"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_17"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3098822.3098834"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-49052-6_4"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2656877.2656890"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2486001.2486011"},{"key":"e_1_3_2_1_7_1","volume-title":"KLEE: Unassisted and Automatic Generation of High-coverage Tests for Complex Systems Programs. In OSDI. 209--224.","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar , Daniel Dunbar , and Dawson Engler . 2008 . KLEE: Unassisted and Automatic Generation of High-coverage Tests for Complex Systems Programs. In OSDI. 209--224. Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: Unassisted and Automatic Generation of High-coverage Tests for Complex Systems Programs. In OSDI. 209--224."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2935634.2935638"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"crossref","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. 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. 337--340.","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1995376.1995394"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1787234.1787259"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2823400"},{"key":"e_1_3_2_1_14_1","unstructured":"Nick Feamster and Hari Balakrishnan. 2005. Detecting BGP configuration faults with static analysis. In NSDI. 43--56.   Nick Feamster and Hari Balakrishnan. 2005. Detecting BGP configuration faults with static analysis. In NSDI. 43--56."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512558"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360220"},{"key":"e_1_3_2_1_17_1","unstructured":"A. Fogel S. Fung L. Pedrosa M. Walraed-Sullivan R. Govindan R. Mahajan and T. Millstein. 2015. A General Approach to Network Configuration Analysis. In NSDI. 469--483.   A. Fogel S. Fung L. Pedrosa M. Walraed-Sullivan R. Govindan R. Mahajan and T. Millstein. 2015. A General Approach to Network Configuration Analysis. In NSDI. 469--483."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677011"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3185467.3185499"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2934872.2934876"},{"key":"e_1_3_2_1_21_1","unstructured":"Ronghui Gu Zhong Shao Hao Chen Xiongnan (Newman) Wu Jieung Kim Vilhelm Sj\u00f6berg and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In OSDI. 653--669.   Ronghui Gu Zhong Shao Hao Chen Xiongnan (Newman) Wu Jieung Kim Vilhelm Sj\u00f6berg and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In OSDI. 653--669."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462178"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"crossref","unstructured":"Arjun Guha Claudiu Saftoiu and Shriram Krishnamurthi. 2010. The essence of JavaScript. In ECOOP. 126--150.   Arjun Guha Claudiu Saftoiu and Shriram Krishnamurthi. 2010. The essence of JavaScript. In ECOOP. 126--150.","DOI":"10.1007\/978-3-642-14107-2_7"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2999572.2999607"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_2_1_26_1","unstructured":"Mukesh Hira and LJ Wobker. 2015. Improving Network Monitoring and Management with Programmable Data Planes. P4 Language Consortium Blog. Available at https:\/\/p4.org\/p4\/inband-network-telemetry\/.  Mukesh Hira and LJ Wobker. 2015. Improving Network Monitoring and Management with Programmable Data Planes. P4 Language Consortium Blog. Available at https:\/\/p4.org\/p4\/inband-network-telemetry\/."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_1_28_1","unstructured":"Xin Jin Xiaozhou Li Haoyu Zhang Nate Foster Jeongkeun Lee Robert Soule Changhoon Kim and Ion Stoica. 2018. NetChain: Scale-Free Sub-RTT Coordination. In NSDI. 35--49.  Xin Jin Xiaozhou Li Haoyu Zhang Nate Foster Jeongkeun Lee Robert Soule Changhoon Kim and Ion Stoica. 2018. NetChain: Scale-Free Sub-RTT Coordination. In NSDI. 35--49."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132764"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27705-4_16"},{"key":"e_1_3_2_1_31_1","unstructured":"Peyman Kazemian. 2017. Network path not found? Forward Networks Blog. Available at https:\/\/bit.ly\/2FzpEEZ.  Peyman Kazemian. 2017. Network path not found? Forward Networks Blog. Available at https:\/\/bit.ly\/2FzpEEZ."},{"key":"e_1_3_2_1_32_1","unstructured":"Peyman Kazemian George Varghese and Nick McKeown. 2012. Header Space Analysis: Static Checking for Networks. In NSDI. 113--126.   Peyman Kazemian George Varghese and Nick McKeown. 2012. Header Space Analysis: Static Checking for Networks. In NSDI. 113--126."},{"key":"e_1_3_2_1_33_1","unstructured":"Ali Kheradmand and Grigore Rosu. 2018. P4K: A Formal Semantics of P4 and Applications. https:\/\/arxiv.org\/abs\/1804.01468.  Ali Kheradmand and Grigore Rosu. 2018. P4K: A Formal Semantics of P4 and Applications. https:\/\/arxiv.org\/abs\/1804.01468."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"crossref","unstructured":"Ahmed Khurshid Xuan Zou Wenxuan Zhou Matthew Caesar and P. Brighten Godfrey. 2013. VeriFlow: Verifying Network-Wide Invariants in Real Time. In NSDI. 15--29.   Ahmed Khurshid Xuan Zou Wenxuan Zhou Matthew Caesar and P. Brighten Godfrey. 2013. VeriFlow: Verifying Network-Wide Invariants in Real Time. In NSDI. 15--29.","DOI":"10.1145\/2342441.2342452"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/279227.279229"},{"key":"e_1_3_2_1_36_1","volume-title":"Dafny: An Automatic Program Verifier for Functional Correctness. In Logic for Programming, Artifical Intelligence, and Reasoning. 348--370.","author":"Leino K. Rustan M.","year":"2010","unstructured":"K. Rustan M. Leino . 2010 . Dafny: An Automatic Program Verifier for Functional Correctness. In Logic for Programming, Artifical Intelligence, and Reasoning. 348--370. K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. In Logic for Programming, Artifical Intelligence, and Reasoning. 348--370."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2004.05.016"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2018436.2018470"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706329"},{"key":"e_1_3_2_1_41_1","unstructured":"Nick McKeown Timon Sloane and Jim Wanderer. 2017. P4 Runtime-Putting the Control Plane in Charge of the Forwarding Plane. Available at http:\/\/bit.ly\/2It6Ecn.  Nick McKeown Timon Sloane and Jim Wanderer. 2017. P4 Runtime-Putting the Control Plane in Charge of the Forwarding Plane. Available at http:\/\/bit.ly\/2It6Ecn."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3185467.3185497"},{"issue":"0","key":"e_1_3_2_1_44_1","first-page":"4","article-title":"P4 Language Specification","volume":"1","author":"P4 Language Consortium","year":"2017","unstructured":"P4 Language Consortium . 2017 . P4 Language Specification , Version 1 . 0 . 4 . Available at https:\/\/p4.org\/specs\/. P4 Language Consortium. 2017. P4 Language Specification, Version 1.0.4. Available at https:\/\/p4.org\/specs\/.","journal-title":"Version"},{"key":"e_1_3_2_1_45_1","unstructured":"P4 Language Consortium. 2017. P4<sub>16<\/sub> Language Specification. https:\/\/p4.org\/p4-spec\/docs\/P4-16-v1.0.0--spec.html.  P4 Language Consortium. 2017. P4<sub>16<\/sub> Language Specification. https:\/\/p4.org\/p4-spec\/docs\/P4-16-v1.0.0--spec.html."},{"key":"e_1_3_2_1_46_1","unstructured":"Aurojit Panda Ori Lahav Katerina J Argyraki Mooly Sagiv and Scott Shenker. 2017. Verifying Reachability in Networks with Mutable Datapaths.. In NSDI. 699--718.   Aurojit Panda Ori Lahav Katerina J Argyraki Mooly Sagiv and Scott Shenker. 2017. Verifying Reachability in Networks with Mutable Datapaths.. In NSDI. 699--718."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837657"},{"key":"e_1_3_2_1_48_1","volume-title":"Advaned Topis in Types and Programming Languages","author":"Pottier Fran\u00e7ois","unstructured":"Fran\u00e7ois Pottier and Didier R\u00e9my . 2005. Advaned Topis in Types and Programming Languages . MIT Press , Chapter The Essence of ML Type Inference, 389--489. Fran\u00e7ois Pottier and Didier R\u00e9my. 2005. Advaned Topis in Types and Programming Languages. MIT Press, Chapter The Essence of ML Type Inference, 389--489."},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3230543.3230548"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2934872.2934881"},{"key":"e_1_3_2_1_51_1","unstructured":"tofino 2015. Barefoot Tofino. https:\/\/www.barefootnetworks.com\/products\/brief-tofino\/.  tofino 2015. Barefoot Tofino. https:\/\/www.barefootnetworks.com\/products\/brief-tofino\/."},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_51"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984012"},{"key":"e_1_3_2_1_54_1","volume-title":"On static reachability analysis of IP networks","author":"Xie Geoffrey G.","unstructured":"Geoffrey G. Xie , Jibin Zhan , David A. Maltz , Hui Zhang , Albert G. Greenberg , G\u00edsli Hj\u00e1lmt\u00fdsson , and Jennifer Rexford . 2005. On static reachability analysis of IP networks . In IEEE INFOCOM. 2170--2183. Geoffrey G. Xie, Jibin Zhan, David A. Maltz, Hui Zhang, Albert G. Greenberg, G\u00edsli Hj\u00e1lmt\u00fdsson, and Jennifer Rexford. 2005. On static reachability analysis of IP networks. In IEEE INFOCOM. 2170--2183."},{"key":"e_1_3_2_1_55_1","volume-title":"Lam","author":"Yang Hongkun","year":"2013","unstructured":"Hongkun Yang and Simon S . Lam . 2013 . Real-time Verification of Network Properties Using Atomic Predicates. In IEEE ICNP. Hongkun Yang and Simon S. Lam. 2013. Real-time Verification of Network Properties Using Atomic Predicates. In IEEE ICNP."},{"key":"e_1_3_2_1_56_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.3230582","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3230543.3230582","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:39:47Z","timestamp":1750210787000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3230543.3230582"}},"subtitle":["practical verification for programmable data planes"],"short-title":[],"issued":{"date-parts":[[2018,8,7]]},"references-count":55,"alternative-id":["10.1145\/3230543.3230582","10.1145\/3230543"],"URL":"https:\/\/doi.org\/10.1145\/3230543.3230582","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"}}]}}