{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,24]],"date-time":"2025-08-24T01:50:05Z","timestamp":1756000205115,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":43,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,11,4]],"date-time":"2020-11-04T00:00:00Z","timestamp":1604448000000},"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,11,4]]},"DOI":"10.1145\/3422604.3425930","type":"proceedings-article","created":{"date-parts":[[2020,10,30]],"date-time":"2020-10-30T00:50:36Z","timestamp":1604019036000},"page":"8-15","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["A General Framework for Compositional Network Modeling"],"prefix":"10.1145","author":[{"given":"Ryan","family":"Beckett","sequence":"first","affiliation":[{"name":"Microsoft Research, Redmond, WA, USA"}]},{"given":"Ratul","family":"Mahajan","sequence":"additional","affiliation":[{"name":"University of Washington & Intentionet, Seattle, WA, USA"}]}],"member":"320","published-online":{"date-parts":[[2020,11,4]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/196244.196379"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_14"},{"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.1145\/3230543.3230583"},{"key":"e_1_3_2_1_5_1","volume-title":"Proc. ACM Program. Lang., 4(POPL)","author":"Beckett R.","year":"2019","unstructured":"R. Beckett , A. Gupta , R. Mahajan , and D. Walker . Abstract interpretation of distributed network control planes . Proc. ACM Program. Lang., 4(POPL) , December 2019 . R. Beckett, A. Gupta, R. Mahajan, and D. Walker. Abstract interpretation of distributed network control planes. Proc. ACM Program. Lang., 4(POPL), December 2019."},{"key":"e_1_3_2_1_6_1","first-page":"127","volume-title":"D. Kosti\u0107, and J. Rexford. A NICE way to test openflow applications. In Presented as part of the 9th USENIX Symposium on Networked Systems Design and Implementation (NSDI 12)","author":"Canini M.","year":"2012","unstructured":"M. Canini , D. Venzano , P. Perev s'ini , D. Kosti\u0107, and J. Rexford. A NICE way to test openflow applications. In Presented as part of the 9th USENIX Symposium on Networked Systems Design and Implementation (NSDI 12) , pages 127 -- 140 , San Jose, CA , 2012 . USENIX. M. Canini, D. Venzano, P. Perev s'ini, D. Kosti\u0107, and J. Rexford. A NICE way to test openflow applications. In Presented as part of the 9th USENIX Symposium on Networked Systems Design and Implementation (NSDI 12), pages 127--140, San Jose, CA, 2012. USENIX."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_1_9_1","first-page":"101","volume-title":"11th USENIX Symposium on Networked Systems Design and Implementation (NSDI 14)","author":"Dobrescu M.","year":"2014","unstructured":"M. Dobrescu and K. Argyraki . Software dataplane verification . In 11th USENIX Symposium on Networked Systems Design and Implementation (NSDI 14) , pages 101 -- 114 , Seattle, WA , 2014 . USENIX Association. M. Dobrescu and K. Argyraki. Software dataplane verification. In 11th USENIX Symposium on Networked Systems Design and Implementation (NSDI 14), pages 101--114, Seattle, WA, 2014. USENIX Association."},{"key":"e_1_3_2_1_10_1","first-page":"217","volume-title":"12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16)","author":"Fayaz S. K.","year":"2016","unstructured":"S. K. Fayaz , T. Sharma , A. Fogel , R. Mahajan , T. Millstein , V. Sekar , and G. Varghese . Efficient network reachability analysis using a succinct control plane representation . In 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16) , pages 217 -- 232 , Savannah, GA , November 2016 . USENIX Association. S. K. Fayaz, T. Sharma, A. Fogel, R. Mahajan, T. Millstein, V. Sekar, and G. Varghese. Efficient network reachability analysis using a succinct control plane representation. In 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16), pages 217--232, Savannah, GA, November 2016. USENIX Association."},{"key":"e_1_3_2_1_11_1","first-page":"469","volume-title":"12th USENIX Symposium on Networked Systems Design and Implementation (NSDI 15)","author":"Fogel A.","year":"2015","unstructured":"A. Fogel , S. Fung , L. Pedrosa , M. Walraed-Sullivan , R. Govindan , R. Mahajan , and T. Millstein . A general approach to network configuration analysis . In 12th USENIX Symposium on Networked Systems Design and Implementation (NSDI 15) , pages 469 -- 483 , Oakland, CA , May 2015 . USENIX Association. A. Fogel, S. Fung, L. Pedrosa, M. Walraed-Sullivan, R. Govindan, R. Mahajan, and T. Millstein. A general approach to network configuration analysis. In 12th USENIX Symposium on Networked Systems Design and Implementation (NSDI 15), pages 469--483, Oakland, CA, May 2015. USENIX Association."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2934872.2934876"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386019"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/LATW.2015.7102519"},{"key":"e_1_3_2_1_16_1","first-page":"680","volume-title":"A tale of two solvers: Eager and lazy approaches to bit-vectors","author":"Hadarean L.","year":"2014","unstructured":"L. Hadarean , K. Bansal , D. Jovanovic , C. Barrett , and C. Tinelli . A tale of two solvers: Eager and lazy approaches to bit-vectors . pages 680 -- 695 , 07 2014 . L. Hadarean, K. Bansal, D. Jovanovic, C. Barrett, and C. Tinelli. A tale of two solvers: Eager and lazy approaches to bit-vectors. pages 680--695, 07 2014."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.17487\/RFC1702"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_2_1_19_1","first-page":"735","volume-title":"14th USENIX Symposium on Networked Systems Design and Implementation (NSDI 17)","author":"Horn A.","year":"2017","unstructured":"A. Horn , A. Kheradmand , and M. Prasad . Delta-net: Real-time network verification using atoms . In 14th USENIX Symposium on Networked Systems Design and Implementation (NSDI 17) , pages 735 -- 749 , Boston, MA , March 2017 . USENIX Association. A. Horn, A. Kheradmand, and M. Prasad. Delta-net: Real-time network verification using atoms. In 14th USENIX Symposium on Networked Systems Design and Implementation (NSDI 17), pages 735--749, Boston, MA, March 2017. USENIX Association."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341302.3342094"},{"key":"e_1_3_2_1_21_1","first-page":"99","volume-title":"Presented as part of the 10th USENIX Symposium on Networked Systems Design and Implementation (NSDI 13)","author":"Kazemian P.","year":"2013","unstructured":"P. Kazemian , M. Chang , H. Zeng , G. Varghese , N. McKeown , and S. Whyte . Real time network policy checking using header space analysis . In Presented as part of the 10th USENIX Symposium on Networked Systems Design and Implementation (NSDI 13) , pages 99 -- 111 , Lombard, IL , 2013 . USENIX. P. Kazemian, M. Chang, H. Zeng, G. Varghese, N. McKeown, and S. Whyte. Real time network policy checking using header space analysis. In Presented as part of the 10th USENIX Symposium on Networked Systems Design and Implementation (NSDI 13), pages 99--111, Lombard, IL, 2013. USENIX."},{"key":"e_1_3_2_1_22_1","first-page":"9","volume-title":"Proceedings of the 9th USENIX Conference on Networked Systems Design and Implementation, NSDI'12","author":"Kazemian P.","year":"2012","unstructured":"P. Kazemian , G. Varghese , and N. McKeown . Header space analysis: Static checking for networks . In Proceedings of the 9th USENIX Conference on Networked Systems Design and Implementation, NSDI'12 , pages 9 -- 9 , Berkeley, CA, USA , 2012 . USENIX Association. P. Kazemian, G. Varghese, and N. McKeown. Header space analysis: Static checking for networks. In Proceedings of the 9th USENIX Conference on Networked Systems Design and Implementation, NSDI'12, pages 9--9, Berkeley, CA, USA, 2012. USENIX Association."},{"key":"e_1_3_2_1_23_1","first-page":"15","volume-title":"Presented as part of the 10th USENIX Symposium on Networked Systems Design and Implementation (NSDI 13)","author":"Khurshid A.","year":"2013","unstructured":"A. Khurshid , X. Zou , W. Zhou , M. Caesar , and P. B. 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) , pages 15 -- 27 , Lombard, IL , 2013 . USENIX. A. Khurshid, X. Zou, W. Zhou, M. Caesar, and P. B. 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), pages 15--27, Lombard, IL, 2013. USENIX."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103675"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2004.1281665"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939141.1939161"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_26"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3230543.3230582"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2018436.2018470"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341302.3342087"},{"key":"e_1_3_2_1_31_1","first-page":"1","volume-title":"Proceedings of the 24th International Conference on Large Installation System Administration, LISA'10","author":"Nelson T.","year":"2010","unstructured":"T. Nelson , C. Barratt , D. J. Dougherty , K. Fisler , and S. Krishnamurthi . The margrave tool for firewall analysis . In Proceedings of the 24th International Conference on Large Installation System Administration, LISA'10 , page 1 -- 8 , USA, 2010 . USENIX Association. T. Nelson, C. Barratt, D. J. Dougherty, K. Fisler, and S. Krishnamurthi. The margrave tool for firewall analysis. In Proceedings of the 24th International Conference on Large Installation System Administration, LISA'10, page 1--8, USA, 2010. USENIX Association."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/3154630.3154687"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.1993.580029"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2807591.2807635"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3230543.3230548"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341302.3342088"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509578.2509586"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594340"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.5555\/1200168"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/INFCOM.2005.1498492"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2015.2398197"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/tnet.2017.2720172"},{"key":"e_1_3_2_1_43_1","first-page":"181","volume-title":"17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 20)","author":"Yuan Y.","year":"2020","unstructured":"Y. Yuan , S.-J. Moon , S. Uppal , L. Jia , and V. Sekar . Netsmc: A custom symbolic model checker for stateful network verification . In 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 20) , pages 181 -- 200 , Santa Clara, CA , February 2020 . USENIX Association. Y. Yuan, S.-J. Moon, S. Uppal, L. Jia, and V. Sekar. Netsmc: A custom symbolic model checker for stateful network verification. In 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 20), pages 181--200, Santa Clara, CA, February 2020. USENIX Association."}],"event":{"name":"HotNets '20: The 19th ACM Workshop on Hot Topics in Networks","sponsor":["SIGCOMM ACM Special Interest Group on Data Communication"],"location":"Virtual Event USA","acronym":"HotNets '20"},"container-title":["Proceedings of the 19th ACM Workshop on Hot Topics in Networks"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3422604.3425930","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3422604.3425930","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:31:28Z","timestamp":1750195888000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3422604.3425930"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11,4]]},"references-count":43,"alternative-id":["10.1145\/3422604.3425930","10.1145\/3422604"],"URL":"https:\/\/doi.org\/10.1145\/3422604.3425930","relation":{},"subject":[],"published":{"date-parts":[[2020,11,4]]},"assertion":[{"value":"2020-11-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}