{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,17]],"date-time":"2025-11-17T12:08:42Z","timestamp":1763381322258,"version":"3.45.0"},"publisher-location":"New York, NY, USA","reference-count":42,"publisher":"ACM","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,11,17]]},"DOI":"10.1145\/3772356.3772380","type":"proceedings-article","created":{"date-parts":[[2025,11,17]],"date-time":"2025-11-17T12:02:48Z","timestamp":1763380968000},"page":"210-217","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Towards Accessible Model-Free Verification"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-2728-1898","authenticated-orcid":false,"given":"Alexander","family":"Krentsel","sequence":"first","affiliation":[{"name":"Google, Mountain View, CA, USA"},{"name":"UC Berkeley, Berkeley, CA, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-0502-6324","authenticated-orcid":false,"given":"Oliver","family":"Ye","sequence":"additional","affiliation":[{"name":"Google, Mountain View, CA, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-2287-2618","authenticated-orcid":false,"given":"Anthony","family":"Tafoya","sequence":"additional","affiliation":[{"name":"Google, Mountain View, CA, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-2320-5414","authenticated-orcid":false,"given":"Xuqian","family":"Ma","sequence":"additional","affiliation":[{"name":"Google, Mountain View, CA, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0524-9425","authenticated-orcid":false,"given":"Sylvia","family":"Ratnasamy","sequence":"additional","affiliation":[{"name":"Google, Mountain View, CA, USA"},{"name":"UC Berkeley, Berkeley, CA, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8041-4841","authenticated-orcid":false,"given":"Anees","family":"Shaikh","sequence":"additional","affiliation":[{"name":"Google, Mountain View, CA, USA"}]}],"member":"320","published-online":{"date-parts":[[2025,11,17]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"2012. Network Verification. https:\/\/www.microsoft.com\/en-us\/research\/project\/network-verification\/. Accessed: 2025-6-21."},{"key":"e_1_3_2_1_2_1","unstructured":"2016. PyBatfish. https:\/\/pybatfish.readthedocs.io\/en\/latest\/. Accessed: 2025-6-10."},{"key":"e_1_3_2_1_3_1","unstructured":"2024. Considerations for large clusters. https:\/\/kubernetes.io\/docs\/setup\/best-practices\/cluster-large\/. Accessed: 2025-6-9."},{"key":"e_1_3_2_1_4_1","unstructured":"2024. vJunos-router Overview. https:\/\/www.juniper.net\/documentation\/us\/en\/software\/vjunos-router\/vjunos-router-kvm\/topics\/vjunos-router-overview-understanding.html. Accessed: 2025-5-8."},{"key":"e_1_3_2_1_5_1","unstructured":"2025. IOL - Cisco Modeling Labs v2.8. https:\/\/developer.cisco.com\/docs\/modeling-labs\/iol\/. Accessed: 2025-5-8."},{"key":"e_1_3_2_1_6_1","volume-title":"Formal Methods for Network Performance Analysis. In 20th USENIX Symposium on Networked Systems Design and Implementation (NSDI 23)","author":"Arashloo Mina Tahmasbi","year":"2023","unstructured":"Mina Tahmasbi Arashloo, Ryan Beckett, and Rachit Agarwal. 2023. Formal Methods for Network Performance Analysis. In 20th USENIX Symposium on Networked Systems Design and Implementation (NSDI 23). USENIX Association, Boston, MA, 645\u2013661. https:\/\/www.usenix.org\/conference\/nsdi23\/presentation\/tahmasbi"},{"key":"e_1_3_2_1_7_1","volume-title":"University of California","author":"Fogel Ari","year":"2015","unstructured":"Ari Fogel and Stanley Fung, University of California, Los Angeles, Luis Pedrosa, University of Southern California, Meg Walraed-Sullivan, Microsoft Research, Ramesh Govindan, University of Southern California, Ratul Mahajan, Microsoft Research, and Todd Millstein, University of California, Los Angeles. [n. d.]. Batfish: A General Approach to Network Configuration Analysis. NSDI 2015 ([n. d.])."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","unstructured":"Daniel O. Awduche Lou Berger Der-Hwa Gan Tony Li Dr. Vijay Srinivasan and George Swallow. 2001. RSVP-TE: Extensions to RSVP for LSP Tunnels. RFC 3209. 10.17487\/RFC3209","DOI":"10.17487\/RFC3209"},{"key":"e_1_3_2_1_9_1","volume-title":"Proceedings of the 2006 conference on Applications, technologies, architectures, and protocols for computer communications. ACM","author":"Bavier Andy","year":"2006","unstructured":"Andy Bavier, Nick Feamster, Mark Huang, Larry Peterson, and Jennifer Rexford. 2006. In VINI veritas: realistic and controlled network experimentation. In Proceedings of the 2006 conference on Applications, technologies, architectures, and protocols for computer communications. ACM, New York, NY, USA."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3098822.3098834"},{"key":"e_1_3_2_1_11_1","unstructured":"bharmarsameer. [n. d.]. BatFish Issue 8981: Traceroute Disagreement. https:\/\/github.com\/batfish\/batfish\/issues\/8981. [Accessed 05-07-2025]."},{"key":"e_1_3_2_1_12_1","volume-title":"Proceedings of the ACM SIGCOMM 2023 Conference (ACM SIGCOMM '23). Association for Computing Machinery","author":"Brown Matt","year":"2023","unstructured":"Matt Brown, Ari Fogel, Daniel Halperin, Victor Heorhiadi, Ratul Mahajan, and Todd Millstein. 2023. Lessons from the evolution of the Batfish configuration analysis tool. In Proceedings of the ACM SIGCOMM 2023 Conference (ACM SIGCOMM '23). Association for Computing Machinery, New York, NY, USA, 122\u2013135."},{"key":"e_1_3_2_1_13_1","volume-title":"Wen Bo Li, et al","author":"Lebsack Carl","year":"2018","unstructured":"Carl Lebsack, Marcus Hines, Paul Borman, Anees Shaikh, Rob Shakir, Wen Bo Li, et al. 2018. gNMI - gRPC Network Management Interface. https:\/\/github.com\/openconfig\/reference\/blob\/master\/rpc\/gnmi\/gnmi-specification.md."},{"key":"e_1_3_2_1_14_1","unstructured":"Roman Dodin. 2021. ContainerLab.Dev. https:\/\/containerlab.dev\/. Accessed: 2025-5-8."},{"key":"e_1_3_2_1_15_1","unstructured":"Roman Dodin. 2021. Nokia SR Linux goes public. https:\/\/netdevops.me\/2021\/nokia-sr-linux-goes-public\/. Accessed: 2025-5-8."},{"key":"e_1_3_2_1_16_1","unstructured":"Tony Fyler. 2023. Azure Outage Disconnects Thousands. https:\/\/techhq.com\/2023\/01\/azure-outage-disconnects-thousands. Accessed: 2024-1-30."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3152434.3152439"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2934872.2934891"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2785956.2787496"},{"key":"e_1_3_2_1_20_1","unstructured":"Dan Halperin. [n. d.]. BatFish Issue 8744: JunOS Parsing Crash. https:\/\/github.com\/batfish\/batfish\/issues\/8744. [Accessed 05-07-2025]."},{"key":"e_1_3_2_1_21_1","unstructured":"Dan Halperin Ari Fogel Ratul Mahajan Victor Heorhiadi Matt Brown Spencer Fraint Todd Millstein Harsh Verma and Corina Miner. 2025. batfish\/batfish. https:\/\/github.com\/batfish\/batfish. https:\/\/github.com\/batfish\/batfish"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/1404014.1404023"},{"key":"e_1_3_2_1_23_1","unstructured":"Marcus Hines and Alex Masi. 2021. Kubernetes Network Emulator. https:\/\/github.com\/openconfig\/kne."},{"key":"e_1_3_2_1_24_1","volume-title":"Details About The October 4 Outage. https:\/\/engineering.fb.com\/2021\/10\/05\/networking-traffic\/outage-details\/. Engineering at Meta (Oct","author":"Janardhan Santosh","year":"2021","unstructured":"Santosh Janardhan. 2021. Details About The October 4 Outage. https:\/\/engineering.fb.com\/2021\/10\/05\/networking-traffic\/outage-details\/. Engineering at Meta (Oct. 2021). Accessed: 2024-1-30."},{"key":"e_1_3_2_1_25_1","volume-title":"Header Space Analysis: Static Checking for Networks. In 9th USENIX Symposium 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 9th USENIX Symposium on Networked Systems Design and Implementation (NSDI 12). 113\u2013126."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2377677.2377766"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1868447.1868466"},{"key":"e_1_3_2_1_28_1","volume-title":"IBM Cloud suffers prolonged outage. TechCrunch (June","author":"Lardinois Frederic","year":"2020","unstructured":"Frederic Lardinois. 2020. IBM Cloud suffers prolonged outage. TechCrunch (June 2020)."},{"key":"e_1_3_2_1_29_1","volume-title":"CrystalNet: Faithfully Emulating Large Production Networks. (October","author":"Liu Hongqiang","year":"2017","unstructured":"Hongqiang Liu, Yibo Zhu, Jitu Padhye, Jiaxin Cao, Sri Tallapragada, Nuno Lopes, Andrey Rybalchenko, Guohan Lu, and Lihua Yuan. 2017. CrystalNet: Faithfully Emulating Large Production Networks. (October 2017), 599\u2013613. https:\/\/www.microsoft.com\/en-us\/research\/publication\/crystalnet-faithfully-emulating-large-production-networks\/"},{"key":"e_1_3_2_1_30_1","unstructured":"Ratul Mahajan. [n. d.]. BatFish Issue 6183: Missing L3 Edge. https:\/\/github.com\/batfish\/batfish\/issues\/6183. [Accessed 05-07-2025]."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2018436.2018470"},{"key":"e_1_3_2_1_32_1","unstructured":"Marcus Hines Rob Shakir Sam Ribeiro Eric Breverman et al. 2018. gNOI - gRPC Network Operations Interface. https:\/\/github.com\/openconfig\/gnoi."},{"key":"e_1_3_2_1_33_1","unstructured":"OpenConfig Project. 2015. OpenConfig. https:\/\/www.openconfig.net\/."},{"key":"e_1_3_2_1_34_1","volume-title":"17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 20)","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. In 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 20). 953\u2013967."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","unstructured":"Yakov Rekhter Susan Hares and Tony Li. 2006. A Border Gateway Protocol 4 (BGP-4). RFC 4271. 10.17487\/RFC4271","DOI":"10.17487\/RFC4271"},{"key":"e_1_3_2_1_36_1","unstructured":"Rob Shakir Xiao Wang Nathaniel Flath et al. 2017. gRIBI - gRPC Routing Information Base Interface. https:\/\/github.com\/openconfig\/gribi."},{"key":"e_1_3_2_1_37_1","unstructured":"Ratul Mahajan Ryan Beckett. 2020. Capturing the state of research on network verification. https:\/\/netverify.fun\/2-current-state-of-research\/. Accessed: 2022-10-9."},{"key":"e_1_3_2_1_38_1","unstructured":"Whitney Sisler and Arista Networks. 2017. Arista Introduces Containerized Software for Cloud Networking - Arista. https:\/\/www.arista.com\/en\/company\/news\/press-release\/2918-pr-20170307. Accessed: 2025-5-8."},{"key":"e_1_3_2_1_39_1","unstructured":"Richard Speed. 2021. AWS runs into IT Problems. https:\/\/www.theregister.com\/2021\/12\/15\/aws_down. Accessed: 2024-1-30."},{"key":"e_1_3_2_1_40_1","unstructured":"WIRED. 2019. The Catch-22 that Broke the Internet. https:\/\/arstechnica.com\/information-technology\/2019\/06\/the-catch-22-that-broke-the-internet\/."},{"key":"e_1_3_2_1_41_1","volume-title":"Proceedings of the ACM SIGCOMM 2024 Conference (ACM SIGCOMM '24). Association for Computing Machinery","author":"Xu Xieyang","year":"2024","unstructured":"Xieyang Xu, Yifei Yuan, Zachary Kincaid, Arvind Krishnamurthy, Ratul Mahajan, David Walker, and Ennan Zhai. 2024. Relational Network Verification. In Proceedings of the ACM SIGCOMM 2024 Conference (ACM SIGCOMM '24). Association for Computing Machinery, New York, NY, USA, 213\u2013227."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3387514.3406217"}],"event":{"name":"HotNets '25: 24th ACM Workshop on Hot Topics in Networks","location":"UMD Campus College Park MD USA","acronym":"HotNets '25","sponsor":["SIGCOMM ACM Special Interest Group on Data Communication"]},"container-title":["Proceedings of the 24th ACM Workshop on Hot Topics in Networks"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3772356.3772380","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,17]],"date-time":"2025-11-17T12:06:14Z","timestamp":1763381174000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3772356.3772380"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,17]]},"references-count":42,"alternative-id":["10.1145\/3772356.3772380","10.1145\/3772356"],"URL":"https:\/\/doi.org\/10.1145\/3772356.3772380","relation":{},"subject":[],"published":{"date-parts":[[2025,11,17]]},"assertion":[{"value":"2025-11-17","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}