{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,13]],"date-time":"2024-08-13T06:40:44Z","timestamp":1723531244797},"publisher-location":"New York, NY, USA","reference-count":27,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,3,28]],"date-time":"2019-03-28T00:00:00Z","timestamp":1553731200000},"content-version":"vor","delay-in-days":365,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1740911"],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["1740911"],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,3,28]]},"DOI":"10.1145\/3185467.3185499","type":"proceedings-article","created":{"date-parts":[[2018,3,23]],"date-time":"2018-03-23T12:30:47Z","timestamp":1521808247000},"update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":48,"title":["Uncovering Bugs in P4 Programs with Assertion-based Verification"],"prefix":"10.1145","author":[{"given":"Lucas","family":"Freire","sequence":"first","affiliation":[{"name":"UFRGS"}]},{"given":"Miguel","family":"Neves","sequence":"additional","affiliation":[{"name":"UFRGS"}]},{"given":"Lucas","family":"Leal","sequence":"additional","affiliation":[{"name":"UFRGS"}]},{"given":"Kirill","family":"Levchenko","sequence":"additional","affiliation":[{"name":"UC San Diego"}]},{"given":"Alberto","family":"Schaeffer-Filho","sequence":"additional","affiliation":[{"name":"UFRGS"}]},{"given":"Marinho","family":"Barcellos","sequence":"additional","affiliation":[{"name":"UFRGS"}]}],"member":"320","published-online":{"date-parts":[[2018,3,28]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2620728.2620743"},{"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":"Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI'08)","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 Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI'08) . USENIX Association, Berkeley, CA, USA, 209--224. http:\/\/dl.acm.org\/citation.cfm?id= 1855741.1855756 Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: Unassisted and Automatic Generation of High-coverage Tests for Complex Systems Programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI'08). USENIX Association, Berkeley, CA, USA, 209--224. http:\/\/dl.acm.org\/citation.cfm?id=1855741.1855756"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/2228298.2228312"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2935634.2935638"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3050220.3050231"},{"key":"e_1_3_2_1_7_1","volume-title":"Software Dataplane Verification. In 11th USENIX Symposium on Networked Systems Design and Implementation (NSDI 14)","author":"Dobrescu Mihai","year":"2014","unstructured":"Mihai Dobrescu and Katerina Argyraki . 2014 . Software Dataplane Verification. In 11th USENIX Symposium on Networked Systems Design and Implementation (NSDI 14) . USENIX Association, Seattle, WA, 101--114. https:\/\/www.usenix.org\/conference\/nsdi14\/technical-sessions\/presentation\/dobrescu Mihai Dobrescu and Katerina Argyraki. 2014. Software Dataplane Verification. In 11th USENIX Symposium on Networked Systems Design and Implementation (NSDI 14). USENIX Association, Seattle, WA, 101--114. https:\/\/www.usenix.org\/conference\/nsdi14\/technical-sessions\/presentation\/dobrescu"},{"key":"e_1_3_2_1_8_1","volume-title":"BUZZ: Testing Context-Dependent Policies in Stateful Networks. In 13th USENIX Symposium on Networked Systems Design and Implementation (NSDI 16)","author":"Fayaz Seyed K.","year":"2016","unstructured":"Seyed K. Fayaz , Tianlong Yu , Yoshiaki Tobioka , Sagar Chaki , and Vyas Sekar . 2016 . BUZZ: Testing Context-Dependent Policies in Stateful Networks. In 13th USENIX Symposium on Networked Systems Design and Implementation (NSDI 16) . USENIX Association, Santa Clara, CA, 275--289. https:\/\/www.usenix.org\/conference\/nsdi16\/technical-sessions\/presentation\/fayaz Seyed K. Fayaz, Tianlong Yu, Yoshiaki Tobioka, Sagar Chaki, and Vyas Sekar. 2016. BUZZ: Testing Context-Dependent Policies in Stateful Networks. In 13th USENIX Symposium on Networked Systems Design and Implementation (NSDI 16). USENIX Association, Santa Clara, CA, 275--289. https:\/\/www.usenix.org\/conference\/nsdi16\/technical-sessions\/presentation\/fayaz"},{"key":"e_1_3_2_1_9_1","unstructured":"Nate Foster Cole Schlesinger Robert Soul\u00e9 and Han Wang. 2017. A Program Logic for Automated P4 Verification. In P4 Workshop. Nate Foster Cole Schlesinger Robert Soul\u00e9 and Han Wang. 2017. A Program Logic for Automated P4 Verification. In P4 Workshop."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3138837"},{"key":"e_1_3_2_1_11_1","volume-title":"Edwards and Nick Ciarleglio","author":"Tomas","year":"2017","unstructured":"Tomas G. Edwards and Nick Ciarleglio . 2017 . Timestamp-Aware RTP Video Switching Using Programmable Data Plan. Industrial Demo. In ACM SIGCOMM. Tomas G. Edwards and Nick Ciarleglio. 2017. Timestamp-Aware RTP Video Switching Using Programmable Data Plan. Industrial Demo. In ACM SIGCOMM."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3050220.3050228"},{"key":"e_1_3_2_1_13_1","volume-title":"Delta-net: Real-time Network Verification Using Atoms. In 14th USENIX Symposium on Networked Systems Design and Implementation (NSDI 17)","author":"Horn Alex","year":"2017","unstructured":"Alex Horn , Ali Kheradmand , and Mukul Prasad . 2017 . Delta-net: Real-time Network Verification Using Atoms. In 14th USENIX Symposium on Networked Systems Design and Implementation (NSDI 17) . USENIX Association, Boston, MA, 735--749. https:\/\/www.usenix.org\/conference\/nsdi17\/technical-sessions\/presentation\/horn-alex Alex Horn, Ali Kheradmand, and Mukul Prasad. 2017. Delta-net: Real-time Network Verification Using Atoms. In 14th USENIX Symposium on Networked Systems Design and Implementation (NSDI 17). USENIX Association, Boston, MA, 735--749. https:\/\/www.usenix.org\/conference\/nsdi17\/technical-sessions\/presentation\/horn-alex"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3050220.3060603"},{"key":"e_1_3_2_1_15_1","volume-title":"Proceedings of the 9th USENIX Conference on Networked Systems Design and Implementation (NSDI'12)","author":"Kazemian Peyman","year":"2012","unstructured":"Peyman Kazemian , George Varghese , and Nick McKeown . 2012 . Header Space Analysis: Static Checking for Networks . In Proceedings of the 9th USENIX Conference on Networked Systems Design and Implementation (NSDI'12) . USENIX Association, Berkeley, CA, USA, 9--9. http:\/\/dl.acm.org\/citation.cfm?id=2228298.2228311 Peyman Kazemian, George Varghese, and Nick McKeown. 2012. Header Space Analysis: Static Checking for Networks. In Proceedings of the 9th USENIX Conference on Networked Systems Design and Implementation (NSDI'12). USENIX Association, Berkeley, CA, USA, 9--9. http:\/\/dl.acm.org\/citation.cfm?id=2228298.2228311"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2342441.2342452"},{"key":"e_1_3_2_1_17_1","unstructured":"The P4.org language consortium. 2017. MRI Exercise. https:\/\/github.com\/p4lang\/tutorials\/blob\/master\/SIGCOMM_2017\/exercises\/mri\/solution\/mri.p4. (2017). The P4.org language consortium. 2017. MRI Exercise. https:\/\/github.com\/p4lang\/tutorials\/blob\/master\/SIGCOMM_2017\/exercises\/mri\/solution\/mri.p4. (2017)."},{"key":"e_1_3_2_1_18_1","unstructured":"The P4.org language consortium. 2017. P4 reference compiler. https:\/\/github.com\/p4lang\/p4c. (2017). The P4.org language consortium. 2017. P4 reference compiler. https:\/\/github.com\/p4lang\/p4c. (2017)."},{"key":"e_1_3_2_1_19_1","unstructured":"The P4.org language consortium. 2018. Switch. https:\/\/github.com\/p4lang\/switch. (2018). The P4.org language consortium. 2018. Switch. https:\/\/github.com\/p4lang\/switch. (2018)."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2999572.2999609"},{"key":"e_1_3_2_1_21_1","volume-title":"Checking Beliefs in Dynamic Networks. In 12th USENIX Symposium on Networked Systems Design and Implementation (NSDI 15)","author":"Lopes Nuno P.","year":"2015","unstructured":"Nuno P. Lopes , Nikolaj Bj\u00f8rner , Patrice Godefroid , Karthick Jayaraman , and George Varghese . 2015 . Checking Beliefs in Dynamic Networks. In 12th USENIX Symposium on Networked Systems Design and Implementation (NSDI 15) . USENIX Association, Oakland, CA, 499--512. https:\/\/www.usenix.org\/conference\/nsdi15\/technical-sessions\/presentation\/lopes Nuno P. Lopes, Nikolaj Bj\u00f8rner, Patrice Godefroid, Karthick Jayaraman, and George Varghese. 2015. Checking Beliefs in Dynamic Networks. In 12th USENIX Symposium on Networked Systems Design and Implementation (NSDI 15). USENIX Association, Oakland, CA, 499--512. https:\/\/www.usenix.org\/conference\/nsdi15\/technical-sessions\/presentation\/lopes"},{"key":"e_1_3_2_1_22_1","volume-title":"Verifying Reachability in Networks with Mutable Datapaths. In 14th USENIX Symposium on Networked Systems Design and Implementation (NSDI 17)","author":"Panda Aurojit","year":"2017","unstructured":"Aurojit Panda , Ori Lahav , Katerina Argyraki , Mooly Sagiv , and Scott Shenker . 2017 . Verifying Reachability in Networks with Mutable Datapaths. In 14th USENIX Symposium on Networked Systems Design and Implementation (NSDI 17) . USENIX Association, Boston, MA, 699--718. https:\/\/www.usenix.org\/conference\/nsdi17\/technical-sessions\/presentation\/panda-mutable-datapaths Aurojit Panda, Ori Lahav, Katerina Argyraki, Mooly Sagiv, and Scott Shenker. 2017. Verifying Reachability in Networks with Mutable Datapaths. In 14th USENIX Symposium on Networked Systems Design and Implementation (NSDI 17). USENIX Association, Boston, MA, 699--718. https:\/\/www.usenix.org\/conference\/nsdi17\/technical-sessions\/presentation\/panda-mutable-datapaths"},{"key":"e_1_3_2_1_23_1","volume-title":"J\u00e9r\u00f4me Fran\u00c3\u011fois, and Olivier Festor.","author":"Signorello Salvatore","year":"2016","unstructured":"Salvatore Signorello , Radu State , J\u00e9r\u00f4me Fran\u00c3\u011fois, and Olivier Festor. 2016 . NDN.p4: Programming information-centric data-planes. In NetSoft . Salvatore Signorello, Radu State, J\u00e9r\u00f4me Fran\u00c3\u011fois, and Olivier Festor. 2016. NDN.p4: Programming information-centric data-planes. In NetSoft."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2774993.2775007"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICC.2013.6654813"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2934872.2934881"},{"key":"e_1_3_2_1_27_1","unstructured":"The P4.org language consortium. 2017. P4_16 Language Specification. https:\/\/p4lang.github.io\/p4-spec\/docs\/P4-16-v1.0.0-spec.html. (2017). Accessed: 2017-11-08. The P4.org language consortium. 2017. P4_16 Language Specification. https:\/\/p4lang.github.io\/p4-spec\/docs\/P4-16-v1.0.0-spec.html. (2017). Accessed: 2017-11-08."}],"event":{"name":"SOSR '18: Symposium on SDN Research","location":"Los Angeles CA USA","acronym":"SOSR '18","sponsor":["SIGCOMM ACM Special Interest Group on Data Communication","ONS Open Networking Summit"]},"container-title":["Proceedings of the Symposium on SDN Research"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3185467.3185499","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3185467.3185499","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,10]],"date-time":"2023-01-10T16:44:36Z","timestamp":1673369076000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3185467.3185499"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,3,28]]},"references-count":27,"alternative-id":["10.1145\/3185467.3185499","10.1145\/3185467"],"URL":"https:\/\/doi.org\/10.1145\/3185467.3185499","relation":{},"subject":[],"published":{"date-parts":[[2018,3,28]]},"assertion":[{"value":"2018-03-28","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}