{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T10:16:27Z","timestamp":1770286587096,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":42,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,8,9]],"date-time":"2021-08-09T00:00:00Z","timestamp":1628467200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61772265, 62072228"],"award-info":[{"award-number":["61772265, 62072228"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"NSF (National Science Foundation)","doi-asserted-by":"publisher","award":["CNS-1834263"],"award-info":[{"award-number":["CNS-1834263"]}],"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":[[2021,8,9]]},"DOI":"10.1145\/3452296.3472937","type":"proceedings-article","created":{"date-parts":[[2021,8,9]],"date-time":"2021-08-09T18:13:15Z","timestamp":1628532795000},"page":"17-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":22,"title":["Aquila"],"prefix":"10.1145","author":[{"given":"Bingchuan","family":"Tian","sequence":"first","affiliation":[{"name":"Nanjing University and Alibaba Group"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jiaqi","family":"Gao","sequence":"additional","affiliation":[{"name":"Harvard University and Alibaba Group"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mengqi","family":"Liu","sequence":"additional","affiliation":[{"name":"Alibaba Group"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ennan","family":"Zhai","sequence":"additional","affiliation":[{"name":"Alibaba Group"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yanqing","family":"Chen","sequence":"additional","affiliation":[{"name":"Nanjing University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yu","family":"Zhou","sequence":"additional","affiliation":[{"name":"Tsinghua University and Alibaba Group"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Li","family":"Dai","sequence":"additional","affiliation":[{"name":"Alibaba Group"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Feng","family":"Yan","sequence":"additional","affiliation":[{"name":"Alibaba Group"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mengjing","family":"Ma","sequence":"additional","affiliation":[{"name":"Alibaba Group"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ming","family":"Tang","sequence":"additional","affiliation":[{"name":"Alibaba Group"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jie","family":"Lu","sequence":"additional","affiliation":[{"name":"Alibaba Group"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xionglie","family":"Wei","sequence":"additional","affiliation":[{"name":"Alibaba Group"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hongqiang Harry","family":"Liu","sequence":"additional","affiliation":[{"name":"Alibaba Group"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ming","family":"Zhang","sequence":"additional","affiliation":[{"name":"Alibaba Group"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Chen","family":"Tian","sequence":"additional","affiliation":[{"name":"Nanjing University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Minlan","family":"Yu","sequence":"additional","affiliation":[{"name":"Harvard University"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,8,9]]},"reference":[{"key":"e_1_3_2_2_1_1","unstructured":"Barefoot Tofino. https:\/\/www.barefootnetworks.com\/products\/brief-tofino.  Barefoot Tofino. https:\/\/www.barefootnetworks.com\/products\/brief-tofino."},{"key":"e_1_3_2_2_2_1","unstructured":"Broadcom's new Trident 4 and Jericho 2 switch devices offer programmability at scale. https:\/\/www.broadcom.com\/blog\/trident4-and-jericho2-offer-programmability-at-scale.  Broadcom's new Trident 4 and Jericho 2 switch devices offer programmability at scale. https:\/\/www.broadcom.com\/blog\/trident4-and-jericho2-offer-programmability-at-scale."},{"key":"e_1_3_2_2_3_1","unstructured":"In-band Network Telemetry (INT) Dataplane Specification. https:\/\/github.com\/p4lang\/p4-applications\/blob\/master\/docs\/INT.pdf.  In-band Network Telemetry (INT) Dataplane Specification. https:\/\/github.com\/p4lang\/p4-applications\/blob\/master\/docs\/INT.pdf."},{"key":"e_1_3_2_2_4_1","unstructured":"NPL 1.3 Specification. https:\/\/github.com\/nplang\/NPL-Spec.  NPL 1.3 Specification. https:\/\/github.com\/nplang\/NPL-Spec."},{"key":"e_1_3_2_2_5_1","unstructured":"ONE Silicon ONE Experience MULTIPLE Roles. https:\/\/blogs.cisco.com\/sp\/one-silicon-one-experience-multiple-roles.  ONE Silicon ONE Experience MULTIPLE Roles. https:\/\/blogs.cisco.com\/sp\/one-silicon-one-experience-multiple-roles."},{"key":"e_1_3_2_2_6_1","first-page":"4","volume-title":"a reference compiler for","unstructured":"p4c , a reference compiler for p 4 programming language. https:\/\/github.com\/p4lang\/p4c. p4c, a reference compiler for p4 programming language. https:\/\/github.com\/p4lang\/p4c."},{"key":"e_1_3_2_2_7_1","unstructured":"P4Runtime. https:\/\/p4.org\/p4-runtime\/.  P4Runtime. https:\/\/p4.org\/p4-runtime\/."},{"key":"e_1_3_2_2_8_1","unstructured":"The switch.p4 program. https:\/\/github.com\/p4lang\/p4c\/tree\/master\/testdata\/p4_14_samples\/switch_20160512.  The switch.p4 program. https:\/\/github.com\/p4lang\/p4c\/tree\/master\/testdata\/p4_14_samples\/switch_20160512."},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3098822.3098834"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2934872.2934909"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2656877.2656890"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_3_2_2_13_1","volume-title":"16th USENIX Symposium on Networked Systems Design and Implementation (NSDI)","author":"Dumitrescu D.","year":"2019","unstructured":"Dumitrescu , D. , Stoenescu , R. , Popovici , M. , Negreanu , L. , and Raiciu , C . Dataplane equivalence and its applications . In 16th USENIX Symposium on Networked Systems Design and Implementation (NSDI) ( 2019 ). Dumitrescu, D., Stoenescu, R., Popovici, M., Negreanu, L., and Raiciu, C. Dataplane equivalence and its applications. In 16th USENIX Symposium on Networked Systems Design and Implementation (NSDI) (2019)."},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373360.3380836"},{"key":"e_1_3_2_2_15_1","volume-title":"12th USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Fayaz S. K.","year":"2016","unstructured":"Fayaz , S. K. , Sharma , T. , Fogel , A. , Mahajan , R. , Millstein , T. , Sekar , V. , and Varghese , G . Efficient network reachability analysis using a succinct control plane representation . In 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI) ( 2016 ). Fayaz, S. K., Sharma, T., Fogel, A., Mahajan, R., Millstein, T., Sekar, V., and Varghese, G. Efficient network reachability analysis using a succinct control plane representation. In 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI) (2016)."},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360220"},{"key":"e_1_3_2_2_17_1","volume-title":"12th USENIX Symposium on Networked Systems Design and Implementation (NSDI)","author":"Fogel A.","year":"2015","unstructured":"Fogel , A. , Fung , S. , Pedrosa , L. , Walraed-Sullivan , M. , Govindan , R. , Mahajan , R. , and Millstein , T . A general approach to network configuration analysis . In 12th USENIX Symposium on Networked Systems Design and Implementation (NSDI) ( 2015 ). Fogel, A., Fung, S., Pedrosa, L., Walraed-Sullivan, M., Govindan, R., Mahajan, R., and Millstein, T. A general approach to network configuration analysis. In 12th USENIX Symposium on Networked Systems Design and Implementation (NSDI) (2015)."},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3365609.3365858"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2934872.2934876"},{"key":"e_1_3_2_2_20_1","volume-title":"14th USENIX Symposium on Networked Systems Design and Implementation (NSDI) (Mar.","author":"Horn A.","year":"2017","unstructured":"Horn , A. , Kheradmand , A. , and Prasad , M. R . Delta-net: Real-time network verification using atoms . In 14th USENIX Symposium on Networked Systems Design and Implementation (NSDI) (Mar. 2017 ). Horn, A., Kheradmand, A., and Prasad, M. R. Delta-net: Real-time network verification using atoms. In 14th USENIX Symposium on Networked Systems Design and Implementation (NSDI) (Mar. 2017)."},{"key":"e_1_3_2_2_22_1","volume-title":"15th USENIX Symposium on Networked Systems Design and Implementation (NSDI)","author":"Jin X.","year":"2018","unstructured":"Jin , X. , Li , X. , Zhang , H. , Foster , N. , Lee , J. , Soul\u00e9 , R. , Kim , C. , and Stoica , I . NetChain: Scale-free sub-RTT coordination . In 15th USENIX Symposium on Networked Systems Design and Implementation (NSDI) ( 2018 ). Jin, X., Li, X., Zhang, H., Foster, N., Lee, J., Soul\u00e9, R., Kim, C., and Stoica, I. NetChain: Scale-free sub-RTT coordination. In 15th USENIX Symposium on Networked Systems Design and Implementation (NSDI) (2018)."},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132764"},{"key":"e_1_3_2_2_24_1","volume-title":"9th USENIX Symposium on Networked Systems Design and Implementation (NSDI)","author":"Kazemian P.","year":"2012","unstructured":"Kazemian , P. , Varghese , G. , and McKeown , N. Header space analysis: Static checking for networks . In 9th USENIX Symposium on Networked Systems Design and Implementation (NSDI) ( 2012 ). Kazemian, P., Varghese, G., and McKeown, N. Header space analysis: Static checking for networks. In 9th USENIX Symposium on Networked Systems Design and Implementation (NSDI) (2012)."},{"key":"e_1_3_2_2_25_1","volume-title":"10th USENIX Symposium on Networked Systems Design and Implementation (NSDI)","author":"Khurshid A.","year":"2013","unstructured":"Khurshid , A. , Zhou , X. , Zhou , W. , Caesar , M. , and Godfrey , P. B . VeriFlow: Verifying network-wide invariants in real time . In 10th USENIX Symposium on Networked Systems Design and Implementation (NSDI) ( 2013 ). Khurshid, A., Zhou, X., Zhou, W., Caesar, M., and Godfrey, P. B. VeriFlow: Verifying network-wide invariants in real time. In 10th USENIX Symposium on Networked Systems Design and Implementation (NSDI) (2013)."},{"key":"e_1_3_2_2_26_1","volume-title":"12th USENIX Symposium on Operating Systems Design and Implementation (OSDI)","author":"Li J.","year":"2016","unstructured":"Li , J. , Michael , E. , Sharma , N. K. , Szekeres , A. , and Ports , D. R. K. Just say NO to Paxos overhead: Replacing consensus with network ordering . In 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI) ( 2016 ). Li, J., Michael, E., Sharma, N. K., Szekeres, A., and Ports, D. R. K. Just say NO to Paxos overhead: Replacing consensus with network ordering. In 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI) (2016)."},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341302.3342085"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"crossref","unstructured":"Liu J. Hallahan W. T. Schlesinger C. Sharif M. Lee J. Soul\u00e9 R. Wang H. Cascaval C. McKeown N. and Foster N. p4v: Practical verification for programmable data planes. In ACM SIGCOMM (SIGCOMM) (2018).  Liu J. Hallahan W. T. Schlesinger C. Sharif M. Lee J. Soul\u00e9 R. Wang H. Cascaval C. McKeown N. and Foster N. p4v: Practical verification for programmable data planes. In ACM SIGCOMM (SIGCOMM) (2018).","DOI":"10.1145\/3230543.3230582"},{"key":"e_1_3_2_2_29_1","volume-title":"12th USENIX Symposium on Networked System Design and Implementation (NSDI)","author":"Lopes N. P.","year":"2015","unstructured":"Lopes , N. P. , Bj\u00f8rner , N. , Godefroid , P. , Jayaraman , K. , and Varghese , G . Checking beliefs in dynamic networks . In 12th USENIX Symposium on Networked System Design and Implementation (NSDI) ( 2015 ). Lopes, N. P., Bj\u00f8rner, N., Godefroid, P., Jayaraman, K., and Varghese, G. Checking beliefs in dynamic networks. In 12th USENIX Symposium on Networked System Design and Implementation (NSDI) (2015)."},{"key":"e_1_3_2_2_30_1","volume-title":"Automatically verifying reachability and well-formedness in P4 networks. Tech. rep","author":"McKeown N.","year":"2016","unstructured":"McKeown , N. , Talayco , D. , Varghese , G. , Lopes , N. , Bj\u00f8rner , N. , and Rybalchenko , A . Automatically verifying reachability and well-formedness in P4 networks. Tech. rep ., 2016 . McKeown, N., Talayco, D., Varghese, G., Lopes, N., Bj\u00f8rner, N., and Rybalchenko, A. Automatically verifying reachability and well-formedness in P4 networks. Tech. rep., 2016."},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3098822.3098824"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3281411.3281421"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3185467.3185497"},{"key":"e_1_3_2_2_34_1","volume-title":"LIPIcs-Leibniz International Proceedings in Informatics","volume":"32","author":"Panda A.","year":"2015","unstructured":"Panda , A. , Argyraki , K. , Sagiv , M. , Schapira , M. , and Shenker , S . New directions for network verification . In LIPIcs-Leibniz International Proceedings in Informatics ( 2015 ), vol. 32 . Panda, A., Argyraki, K., Sagiv, M., Schapira, M., and Shenker, S. New directions for network verification. In LIPIcs-Leibniz International Proceedings in Informatics (2015), vol. 32."},{"key":"e_1_3_2_2_35_1","volume-title":"14th USENIX Symposium on Networked Systems Design and Implementation (NSDI)","author":"Panda A.","year":"2017","unstructured":"Panda , A. , Lahav , O. , Argyraki , K. J. , Sagiv , M. , and Shenker , S . Verifying reachability in networks with mutable datapaths . In 14th USENIX Symposium on Networked Systems Design and Implementation (NSDI) ( 2017 ). Panda, A., Lahav, O., Argyraki, K. J., Sagiv, M., and Shenker, S. Verifying reachability in networks with mutable datapaths. In 14th USENIX Symposium on Networked Systems Design and Implementation (NSDI) (2017)."},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/MNET.2005.1470677"},{"key":"e_1_3_2_2_37_1","volume-title":"14th USENIX Symposium on Networked Systems Design and Implementation (NSDI)","author":"Sharma N. K.","year":"2017","unstructured":"Sharma , N. K. , Kaufmann , A. , Anderson , T. , Krishnamurthy , A. , Nelson , J. , and Peter , S . Evaluating the power of flexible packet processing for network resource allocation . In 14th USENIX Symposium on Networked Systems Design and Implementation (NSDI) ( 2017 ). Sharma, N. K., Kaufmann, A., Anderson, T., Krishnamurthy, A., Nelson, J., and Peter, S. Evaluating the power of flexible packet processing for network resource allocation. In 14th USENIX Symposium on Networked Systems Design and Implementation (NSDI) (2017)."},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2934872.2934900"},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3230543.3230548"},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2934872.2934881"},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_51"},{"key":"e_1_3_2_2_42_1","volume-title":"FSR: Formal analysis and implementation toolkit for safe interdomain routing","author":"Wang A.","year":"2012","unstructured":"Wang , A. , Jia , L. , Zhou , W. , Ren , Y. , Loo , B. T. , Rexford , J. , Nigam , V. , Scedrov , A. , and Talcott , C. L . FSR: Formal analysis and implementation toolkit for safe interdomain routing . IEEE\/ACM Transactions on Network (ToN) 20, 6 ( 2012 ), 1814--1827. Wang, A., Jia, L., Zhou, W., Ren, Y., Loo, B. T., Rexford, J., Nigam, V., Scedrov, A., and Talcott, C. L. FSR: Formal analysis and implementation toolkit for safe interdomain routing. IEEE\/ACM Transactions on Network (ToN) 20, 6 (2012), 1814--1827."},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.14778\/3368289.3368301"}],"event":{"name":"SIGCOMM '21: ACM SIGCOMM 2021 Conference","location":"Virtual Event USA","acronym":"SIGCOMM '21","sponsor":["SIGCOMM ACM Special Interest Group on Data Communication"]},"container-title":["Proceedings of the 2021 ACM SIGCOMM 2021 Conference"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3452296.3472937","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3452296.3472937","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3452296.3472937","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:17:40Z","timestamp":1750191460000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3452296.3472937"}},"subtitle":["a practically usable verification system for production-scale programmable data planes"],"short-title":[],"issued":{"date-parts":[[2021,8,9]]},"references-count":42,"alternative-id":["10.1145\/3452296.3472937","10.1145\/3452296"],"URL":"https:\/\/doi.org\/10.1145\/3452296.3472937","relation":{},"subject":[],"published":{"date-parts":[[2021,8,9]]},"assertion":[{"value":"2021-08-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}