{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,27]],"date-time":"2026-01-27T12:11:23Z","timestamp":1769515883921,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":27,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T00:00:00Z","timestamp":1693526400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,9,10]]},"DOI":"10.1145\/3603269.3604842","type":"proceedings-article","created":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T16:16:29Z","timestamp":1693584989000},"page":"94-107","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":19,"title":["Lightyear: Using Modularity to Scale BGP Control Plane Verification"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-9696-2914","authenticated-orcid":false,"given":"Alan","family":"Tang","sequence":"first","affiliation":[{"name":"UCLA, Los Angeles, California, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7844-2026","authenticated-orcid":false,"given":"Ryan","family":"Beckett","sequence":"additional","affiliation":[{"name":"Microsoft, Redmond, Washington, United States of America"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-5786-5542","authenticated-orcid":false,"given":"Steven","family":"Benaloh","sequence":"additional","affiliation":[{"name":"Microsoft, Redmond, Washington, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-9502-9360","authenticated-orcid":false,"given":"Karthick","family":"Jayaraman","sequence":"additional","affiliation":[{"name":"Microsoft, Redmond, Washington, United States"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-8073-9943","authenticated-orcid":false,"given":"Tejas","family":"Patil","sequence":"additional","affiliation":[{"name":"Microsoft, Redmond, Washington, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2031-1514","authenticated-orcid":false,"given":"Todd","family":"Millstein","sequence":"additional","affiliation":[{"name":"UCLA, Los Angeles, California, United States"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8218-5701","authenticated-orcid":false,"given":"George","family":"Varghese","sequence":"additional","affiliation":[{"name":"UCLA, Los Angeles, California, USA"}]}],"member":"320","published-online":{"date-parts":[[2023,9]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Tiramisu: Fast Multilayer Network Verification. In 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 20)","author":"Abhashkumar Anubhavnidhi","year":"2020","unstructured":"Anubhavnidhi Abhashkumar, Aaron Gember-Jacobson, and Aditya Akella. 2020. Tiramisu: Fast Multilayer Network Verification. In 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 20). USENIX Association, Santa Clara, CA, 201--219. https:\/\/www.usenix.org\/conference\/nsdi20\/presentation\/abhashkumar"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591222"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535862"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3098822.3098834"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3230543.3230583"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371110"},{"key":"e_1_3_2_1_7_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"de Moura Leonardo","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, C. R. Ramakrishnan and Jakob Rehof (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 337--340."},{"key":"e_1_3_2_1_8_1","volume-title":"Proceedings of the 2Nd Conference on Symposium on Networked Systems Design & Implementation -","volume":"2","author":"Feamster Nick","year":"2005","unstructured":"Nick Feamster and Hari Balakrishnan. 2005. Detecting BGP Configuration Faults with Static Analysis. In Proceedings of the 2Nd Conference on Symposium on Networked Systems Design & Implementation - Volume 2 (NSDI'05). USENIX Association, Berkeley, CA, USA, 43--56. http:\/\/dl.acm.org\/citation.cfm?id=1251203.1251207"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0243-x"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2934872.2934876"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341302.3342094"},{"key":"e_1_3_2_1_14_1","volume-title":"Proceedings of IFIP '83","author":"Jones C. B.","year":"1983","unstructured":"C. B. Jones. 1983. Specification and design of (parallel) programs. In Proceedings of IFIP '83, R. E. A. Manson (Ed.). IFIP, North-Holland, 321--332."},{"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"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2377677.2377766"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"e_1_3_2_1_18_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"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2043164.2018470"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837657"},{"key":"e_1_3_2_1_21_1","volume-title":"Krzysztof R. Apt (Ed.)","volume":"13","author":"Pnueli Amir","year":"1984","unstructured":"Amir Pnueli. 1984. In Transition From Global to Modular Temporal Reasoning about Programs. In Logics and Models of Concurrent Systems (NATO ASI Series), Krzysztof R. Apt (Ed.), Vol. 13. Springer, 123--144."},{"key":"e_1_3_2_1_22_1","volume-title":"Ali Kheradmand, Brighten Godfrey, and Matthew Caesar.","author":"Prabhu Santhosh","year":"2020","unstructured":"Santhosh Prabhu, Kuan Yen Chou, Ali Kheradmand, Brighten Godfrey, and Matthew Caesar. 2020. Plankton: Scalable network configuration verification through model checking. (2020)."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","unstructured":"Tim Alberdingk Thijm Ryan Beckett Aarti Gupta and David Walker. 2022. Kirigami the Verifiable Art of Network Cutting. (2022). 10.48550\/ARXIV.2202.06098","DOI":"10.48550\/ARXIV.2202.06098"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3022671.2984012"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2015.2398197"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3387514.3406217"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3387514.3406217"},{"key":"e_1_3_2_1_28_1","unstructured":"Zen [n. d.]. Zen. https:\/\/github.com\/microsoft\/Zen. ([n. d.])."}],"event":{"name":"ACM SIGCOMM '23: ACM SIGCOMM 2023 Conference","location":"New York NY USA","acronym":"ACM SIGCOMM '23","sponsor":["SIGCOMM ACM Special Interest Group on Data Communication"]},"container-title":["Proceedings of the ACM SIGCOMM 2023 Conference"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3603269.3604842","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3603269.3604842","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:46:42Z","timestamp":1750178802000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3603269.3604842"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,9]]},"references-count":27,"alternative-id":["10.1145\/3603269.3604842","10.1145\/3603269"],"URL":"https:\/\/doi.org\/10.1145\/3603269.3604842","relation":{},"subject":[],"published":{"date-parts":[[2023,9]]},"assertion":[{"value":"2023-09-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}