{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T07:20:48Z","timestamp":1770276048119,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":34,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,7,30]],"date-time":"2020-07-30T00:00:00Z","timestamp":1596067200000},"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":[[2020,7,30]]},"DOI":"10.1145\/3387514.3405888","type":"proceedings-article","created":{"date-parts":[[2020,7,30]],"date-time":"2020-07-30T22:35:31Z","timestamp":1596148531000},"page":"571-585","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":26,"title":["bf4"],"prefix":"10.1145","author":[{"given":"Dragos","family":"Dumitrescu","sequence":"first","affiliation":[{"name":"University Politehnica of Bucharest"}]},{"given":"Radu","family":"Stoenescu","sequence":"additional","affiliation":[{"name":"University Politehnica of Bucharest"}]},{"given":"Lorina","family":"Negreanu","sequence":"additional","affiliation":[{"name":"University Politehnica of Bucharest"}]},{"given":"Costin","family":"Raiciu","sequence":"additional","affiliation":[{"name":"University Politehnica of Bucharest"}]}],"member":"320","published-online":{"date-parts":[[2020,7,30]]},"reference":[{"key":"e_1_3_2_2_1_1","volume-title":"by Hana Chockler and Georg Weissenbacher","author":"Abate Alessandro","year":"2018","unstructured":"Alessandro Abate , Cristina David , Pascal Kesseli , Daniel Kroening , and Elizabeth Polgreen . \" Counterexample Guided Inductive Synthesis Modulo Theories\". In: Computer Aided Verification. Ed. by Hana Chockler and Georg Weissenbacher . Springer International Publishing , 2018 . Alessandro Abate, Cristina David, Pascal Kesseli, Daniel Kroening, and Elizabeth Polgreen. \"Counterexample Guided Inductive Synthesis Modulo Theories\". In: Computer Aided Verification. Ed. by Hana Chockler and Georg Weissenbacher. Springer International Publishing, 2018."},{"key":"e_1_3_2_2_2_1","volume-title":"Compilers: Principles, Techniques, and Tools","author":"Aho Alfred V.","year":"2006","unstructured":"Alfred V. Aho , Monica S. Lam , Ravi Sethi , and Jeffrey D. Ullman . Compilers: Principles, Techniques, and Tools ( 2 nd Edition). Addison Wesley , Aug. 2006 . isbn: 0321486811. url: http:\/\/www.amazon.ca\/exec\/obidos\/redirect?tag=citeulike09-20%5C&path=ASIN\/0321486811. Alfred V. Aho, Monica S. Lam, Ravi Sethi, and Jeffrey D. Ullman. Compilers: Principles, Techniques, and Tools (2nd Edition). Addison Wesley, Aug. 2006. isbn: 0321486811. url: http:\/\/www.amazon.ca\/exec\/obidos\/redirect?tag=citeulike09-20%5C&path=ASIN\/0321486811.","edition":"2"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2018.00074"},{"key":"e_1_3_2_2_4_1","volume-title":"SIGCOMM.","author":"Beckett Ryan","year":"2017","unstructured":"Ryan Beckett , Aarti Gupta , Ratul Mahajan , and David Walker . \" A General Approach to Network Configuration Verification\". In: SIGCOMM. 2017 . Ryan Beckett, Aarti Gupta, Ratul Mahajan, and David Walker. \"A General Approach to Network Configuration Verification\". In: SIGCOMM. 2017."},{"key":"e_1_3_2_2_5_1","first-page":"437","volume-title":"Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI 2017. Barcelona, Spain: ACM","author":"Beckett Ryan","year":"2017","unstructured":"Ryan Beckett , Ratul Mahajan , Todd Millstein , Jitendra Padhye , and David Walker . \" Network Configuration Synthesis with Abstract Topologies\". In: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI 2017. Barcelona, Spain: ACM , 2017 , pp. 437 -- 451 . isbn: 978-1-4503-4988-8. doi: 10.1145\/3062341.3062367. url: http:\/\/doi.acm.org\/10.1145\/3062341.3062367. Ryan Beckett, Ratul Mahajan, Todd Millstein, Jitendra Padhye, and David Walker. \"Network Configuration Synthesis with Abstract Topologies\". In: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI 2017. Barcelona, Spain: ACM, 2017, pp. 437--451. isbn: 978-1-4503-4988-8. doi: 10.1145\/3062341.3062367. url: http:\/\/doi.acm.org\/10.1145\/3062341.3062367."},{"key":"e_1_3_2_2_6_1","first-page":"70","volume-title":"by Ranjit Jhala and David Schmidt.","author":"Bradley Aaron R.","year":"2011","unstructured":"Aaron R. Bradley . \"SAT- Based Model Checking without Unrolling\". In: Verification, Model Checking, and Abstract Interpretation. Ed. by Ranjit Jhala and David Schmidt. Berlin, Heidelberg : Springer Berlin Heidelberg , 2011 , pp. 70 -- 87 . isbn: 978-3-642-18275-4. Aaron R. Bradley. \"SAT-Based Model Checking without Unrolling\". In: Verification, Model Checking, and Abstract Interpretation. Ed. by Ranjit Jhala and David Schmidt. Berlin, Heidelberg: Springer Berlin Heidelberg, 2011, pp. 70--87. isbn: 978-3-642-18275-4."},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3139645.3139648"},{"key":"e_1_3_2_2_8_1","volume-title":"Proc. NSDI'12","author":"Canini Marco","unstructured":"Marco Canini , Daniele Venzano , Peter Peresini , Dejan Kosti\u0107 , and Jennifer Rexford . \" A NICE Way to Test Openflow Applications\". In: Proc. NSDI'12 . Marco Canini, Daniele Venzano, Peter Peresini, Dejan Kosti\u0107, and Jennifer Rexford. \"A NICE Way to Test Openflow Applications\". In: Proc. NSDI'12."},{"key":"e_1_3_2_2_9_1","volume-title":"Hardware and Software: Verification and Testing. Ed. by Armin Biere, Amir Nahir, and Tanja Vos.","author":"Chockler Hana","year":"2013","unstructured":"Hana Chockler , Alexander Ivrii , and Arie Matsliah . \" Computing Interpolants without Proofs\". In: Hardware and Software: Verification and Testing. Ed. by Armin Biere, Amir Nahir, and Tanja Vos. Berlin, Heidelberg : Springer Berlin Heidelberg , 2013 . Hana Chockler, Alexander Ivrii, and Arie Matsliah. \"Computing Interpolants without Proofs\". In: Hardware and Software: Verification and Testing. Ed. by Armin Biere, Amir Nahir, and Tanja Vos. Berlin, Heidelberg: Springer Berlin Heidelberg, 2013."},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011276507260"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35873-9_10"},{"key":"e_1_3_2_2_12_1","first-page":"150","volume-title":"by Ranjit Jhala and David Schmidt.","author":"Cousot Patrick","year":"2011","unstructured":"Patrick Cousot , Radhia Cousot , and Francesco Logozzo . \" Precondition Inference from Intermittent Assertions and Application to Contracts on Collections\". In: Verification, Model Checking, and Abstract Interpretation. Ed. by Ranjit Jhala and David Schmidt. Berlin, Heidelberg : Springer Berlin Heidelberg , 2011 , pp. 150 -- 168 . ISBN: 978-3-642-18275-4. Patrick Cousot, Radhia Cousot, and Francesco Logozzo. \"Precondition Inference from Intermittent Assertions and Application to Contracts on Collections\". In: Verification, Model Checking, and Abstract Interpretation. Ed. by Ranjit Jhala and David Schmidt. Berlin, Heidelberg: Springer Berlin Heidelberg, 2011, pp. 150--168. ISBN: 978-3-642-18275-4."},{"key":"e_1_3_2_2_13_1","volume-title":"Proc. TACAS'08","author":"Moura Leonardo De","unstructured":"Leonardo De Moura and Nikolaj Bj\u00f8rner . \"Z3 : An Efficient SMT Solver \". In: Proc. TACAS'08 . Leonardo De Moura and Nikolaj Bj\u00f8rner. \"Z3: An Efficient SMT Solver\". In: Proc. TACAS'08."},{"key":"e_1_3_2_2_14_1","volume-title":"Symposium on SDN Research (SOSR)","author":"Dumitru Mihai","year":"2020","unstructured":"Mihai Dumitru , Dragos Dumitrescu , and Costin Raiciu . \" Is it possible to exploit buggy P4 programs?\" In : Symposium on SDN Research (SOSR) . 2020 . Mihai Dumitru, Dragos Dumitrescu, and Costin Raiciu. \"Is it possible to exploit buggy P4 programs?\" In: Symposium on SDN Research (SOSR). 2020."},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360220"},{"key":"e_1_3_2_2_16_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_2_17_1","volume-title":"SIGCOMM.","author":"Gember-Jacobson Aaron","year":"2016","unstructured":"Aaron Gember-Jacobson , Raajay Viswanathan , Aditya Akella , and Ratul Mahajan . \" Fast Control Plane Analysis Using an Abstract Representation\". In: SIGCOMM. 2016 . Aaron Gember-Jacobson, Raajay Viswanathan, Aditya Akella, and Ratul Mahajan. \"Fast Control Plane Analysis Using an Abstract Representation\". In: SIGCOMM. 2016."},{"key":"e_1_3_2_2_18_1","first-page":"579","volume-title":"15th USENIX Symposium on Networked Systems Design and Implementation (NSDI 18)","author":"El-Hassany Ahmed","year":"2018","unstructured":"Ahmed El-Hassany , Petar Tsankov , Laurent Vanbever , and Martin Vechev . \"NetComplete : Practical Network-Wide Configuration Synthesis with Autocompletion \". In: 15th USENIX Symposium on Networked Systems Design and Implementation (NSDI 18) . Renton, WA: USENIX Association , 2018 , pp. 579 -- 594 . isbn: 978-1-931971-43-0. url: https:\/\/www.usenix.org\/conference\/nsdi18\/presentation\/el-hassany. Ahmed El-Hassany, Petar Tsankov, Laurent Vanbever, and Martin Vechev. \"NetComplete: Practical Network-Wide Configuration Synthesis with Autocompletion\". In: 15th USENIX Symposium on Networked Systems Design and Implementation (NSDI 18). Renton, WA: USENIX Association, 2018, pp. 579--594. isbn: 978-1-931971-43-0. url: https:\/\/www.usenix.org\/conference\/nsdi18\/presentation\/el-hassany."},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/77606.77608"},{"key":"e_1_3_2_2_20_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_2_21_1","first-page":"15","article-title":"VeriFlow: Verifying Network-Wide Invariants in Real Time","author":"Khurshid Ahmed","year":"2013","unstructured":"Ahmed Khurshid , Xuan Zou , Wenxuan Zhou , Matthew Caesar , and P. Brighten Godfrey . \" VeriFlow: Verifying Network-Wide Invariants in Real Time \". In: Presented as part of the 10th USENIX Symposium on Networked Systems Design and Implementation (NSDI 13). Lombard , IL : USENIX, 2013 , pp. 15 -- 27 . isbn: 978-1-931971-00-3. url: https:\/\/www.usenix.org\/conference\/nsdi13\/technical-sessions\/presentation\/khurshid. Ahmed Khurshid, Xuan Zou, Wenxuan Zhou, Matthew Caesar, and P. Brighten Godfrey. \"VeriFlow: Verifying Network-Wide Invariants in Real Time\". In: Presented as part of the 10th USENIX Symposium on Networked Systems Design and Implementation (NSDI 13). Lombard, IL: USENIX, 2013, pp. 15--27. isbn: 978-1-931971-00-3. url: https:\/\/www.usenix.org\/conference\/nsdi13\/technical-sessions\/presentation\/khurshid.","journal-title":"Lombard"},{"key":"e_1_3_2_2_22_1","first-page":"424","volume-title":"by Thomas Ball and Robert B. Jones.","author":"Lahiri Shuvendu K.","year":"2006","unstructured":"Shuvendu K. Lahiri , Robert Nieuwenhuis , and Albert Oliveras . \" SMT Techniques for Fast Predicate Abstraction\". In: Computer Aided Verification. Ed. by Thomas Ball and Robert B. Jones. Berlin, Heidelberg : Springer Berlin Heidelberg , 2006 , pp. 424 -- 437 . ISBN: 978-3-540-37411-4. Shuvendu K. Lahiri, Robert Nieuwenhuis, and Albert Oliveras. \"SMT Techniques for Fast Predicate Abstraction\". In: Computer Aided Verification. Ed. by Thomas Ball and Robert B. Jones. Berlin, Heidelberg: Springer Berlin Heidelberg, 2006, pp. 424--437. ISBN: 978-3-540-37411-4."},{"key":"e_1_3_2_2_23_1","volume-title":"Proc. of the 26th Symposium on Operating Systems Principles (SOSP).","author":"Liu Hongqiang Harry","unstructured":"Hongqiang Harry Liu , Yibo Zhu , Jitu Padhye , Jiaxin Cao , Sri Tallapragada , Nuno P. Lopes , Andrey Rybalchenko , Guohan Lu , and Lihua Yuan . \"CrystalNet : Faithfully Emulating Large Production Networks \". In: Proc. of the 26th Symposium on Operating Systems Principles (SOSP). Hongqiang Harry Liu, Yibo Zhu, Jitu Padhye, Jiaxin Cao, Sri Tallapragada, Nuno P. Lopes, Andrey Rybalchenko, Guohan Lu, and Lihua Yuan. \"CrystalNet: Faithfully Emulating Large Production Networks\". In: Proc. of the 26th Symposium on Operating Systems Principles (SOSP)."},{"key":"e_1_3_2_2_24_1","volume-title":"Proceedings of ACM SIGCOMM","author":"Liu Jed","year":"2018","unstructured":"Jed Liu , William Hallahan , Cole Schlesinger , Milad Sharif , Jeongkeun Lee , Robert Soule , Han Wang , Calin Cascaval , Nick McKeown , and Nate Foster . \"p4v : Practical Verification for Programmable Data Planes \". In: Proceedings of ACM SIGCOMM 2018 . Jed Liu, William Hallahan, Cole Schlesinger, Milad Sharif, Jeongkeun Lee, Robert Soule, Han Wang, Calin Cascaval, Nick McKeown, and Nate Foster. \"p4v: Practical Verification for Programmable Data Planes\". In: Proceedings of ACM SIGCOMM 2018."},{"key":"e_1_3_2_2_25_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_2_26_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 . 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. 2016. url: https:\/\/www.microsoft.com\/en-us\/research\/publication\/automatically-verifying-reachability-well-formedness-p4-networks\/."},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3281411.3281421"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3185467.3185497"},{"key":"e_1_3_2_2_29_1","unstructured":"ONOS. Peacock. Open Network Operating System. 2019.  ONOS. Peacock. Open Network Operating System. 2019."},{"key":"e_1_3_2_2_30_1","volume-title":"v1.1.0. The P4 Language Consortium","author":"Specification Language","year":"2018","unstructured":"P4_16 Language Specification . v1.1.0. The P4 Language Consortium . Nov. 2018 . P4_16 Language Specification. v1.1.0. The P4 Language Consortium. Nov. 2018."},{"key":"e_1_3_2_2_31_1","volume-title":"v1.0.0. The P4.org API Working Group","author":"Specification Runtime","year":"2019","unstructured":"P4 Runtime Specification . v1.0.0. The P4.org API Working Group . Jan. 2019 . P4Runtime Specification. v1.0.0. The P4.org API Working Group. Jan. 2019."},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3230543.3230548"},{"key":"e_1_3_2_2_33_1","volume-title":"Scalable symbolic execution for modern networks","author":"Stoenescu Radu","year":"2016","unstructured":"Radu Stoenescu , Matei Popovici , Lorina Negreanu , and Costin Raiciu . \"SymNet : Scalable symbolic execution for modern networks \". In : SIGCOMM. 2016 . doi: 10.1145\/2934872.2934881. url: http:\/\/doi.acm.org\/10.1145\/2934872.2934881. Radu Stoenescu, Matei Popovici, Lorina Negreanu, and Costin Raiciu. \"SymNet: Scalable symbolic execution for modern networks\". In: SIGCOMM. 2016. doi: 10.1145\/2934872.2934881. url: http:\/\/doi.acm.org\/10.1145\/2934872.2934881."},{"key":"e_1_3_2_2_34_1","first-page":"439","volume-title":"Proceedings of the 5th International Conference on Software Engineering. ICSE 81","author":"Weiser Mark","year":"1981","unstructured":"Mark Weiser . \" Program Slicing\". In: Proceedings of the 5th International Conference on Software Engineering. ICSE 81 . San Diego, California, USA: IEEE Press , 1981 , pp. 439 -- 449 . ISBN: 0897911466. Mark Weiser. \"Program Slicing\". In: Proceedings of the 5th International Conference on Software Engineering. ICSE 81. San Diego, California, USA: IEEE Press, 1981, pp. 439--449. ISBN: 0897911466."}],"event":{"name":"SIGCOMM '20: Annual conference of the ACM Special Interest Group on Data Communication on the applications, technologies, architectures, and protocols for computer communication","location":"Virtual Event USA","acronym":"SIGCOMM '20","sponsor":["SIGCOMM ACM Special Interest Group on Data Communication"]},"container-title":["Proceedings of the Annual conference of the ACM Special Interest Group on Data Communication on the applications, technologies, architectures, and protocols for computer communication"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3387514.3405888","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3387514.3405888","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:41:36Z","timestamp":1750200096000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3387514.3405888"}},"subtitle":["towards bug-free P4 programs"],"short-title":[],"issued":{"date-parts":[[2020,7,30]]},"references-count":34,"alternative-id":["10.1145\/3387514.3405888","10.1145\/3387514"],"URL":"https:\/\/doi.org\/10.1145\/3387514.3405888","relation":{},"subject":[],"published":{"date-parts":[[2020,7,30]]},"assertion":[{"value":"2020-07-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}