{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T16:31:31Z","timestamp":1777566691252,"version":"3.51.4"},"publisher-location":"New York, NY, USA","reference-count":40,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,11,18]],"date-time":"2024-11-18T00:00:00Z","timestamp":1731888000000},"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":[[2024,11,18]]},"DOI":"10.1145\/3696348.3696865","type":"proceedings-article","created":{"date-parts":[[2024,11,11]],"date-time":"2024-11-11T00:20:52Z","timestamp":1731284452000},"page":"237-245","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Lightweight Automated Reasoning for Network Architectures"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5071-902X","authenticated-orcid":false,"given":"Rahul","family":"Bothra","sequence":"first","affiliation":[{"name":"UIUC"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2192-1469","authenticated-orcid":false,"given":"Venkat","family":"Arun","sequence":"additional","affiliation":[{"name":"UT Austin"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-2930-1982","authenticated-orcid":false,"given":"Brighten","family":"Godfrey","sequence":"additional","affiliation":[{"name":"UIUC and Broadcom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6626-141X","authenticated-orcid":false,"given":"Akshay","family":"Narayan","sequence":"additional","affiliation":[{"name":"Brown University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0498-0854","authenticated-orcid":false,"given":"Ahmed","family":"Saeed","sequence":"additional","affiliation":[{"name":"Georgia Tech"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,11,18]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"crossref","unstructured":"Mohammad Alizadeh Albert G. Greenberg David A. Maltz Jitendra Padhye Parveen Patel Balaji Prabhakar Sudipta Sengupta and Murari Sridharan. 2010. Data Center TCP (DCTCP). In SIGCOMM.","DOI":"10.1145\/1851182.1851192"},{"key":"e_1_3_2_1_2_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Barbosa Haniel","unstructured":"Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres N\u00f6tzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. 2022. cvc5: A Versatile and Industrial-Strength SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems, Dana Fisman and Grigore Rosu (Eds.). Springer International Publishing, Cham, 415--442."},{"key":"e_1_3_2_1_3_1","volume-title":"Peterson","author":"Brakmo Lawrence S.","year":"1994","unstructured":"Lawrence S. Brakmo, Sean W. O'Malley, and Larry L. Peterson. 1994. TCP Vegas: New Techniques for Congestion Detection and Avoidance. In SIGCOMM."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","unstructured":"Qizhe Cai Midhul Vuppalapati Jaehyun Hwang Christos Kozyrakis and Rachit Agarwal. 2022. Towards μs Tail Latency and Terabit Ethernet: Disaggregating the Host Network Stack. In SIGCOMM. https:\/\/doi.org\/10.1145\/3544216.3544230","DOI":"10.1145\/3544216.3544230"},{"key":"e_1_3_2_1_5_1","unstructured":"Michael Dalton David Schultz Jacob Adriaens Ahsan Arefin Anshuman Gupta Brian Fahs Dima Rubinstein Enrique Candromeda Zermeno Erik Rubow James Alexander Docauer Jesse Alpert Jing Ai Jon Olson Kevin DeCabooter Marc de Kruijf Nan Hua Nathan Lewis Nikhil Kasinadhuni Riccardo Crepaldi Srinivas Krishnan Subbaiah Venkata Yossi Richter Uday Naik and Amin Vahdat. 2018. Andromeda: Performance Isolation and Velocity at Scale in Cloud Network Virtualization. In NSDI."},{"key":"e_1_3_2_1_6_1","volume-title":"Z3: an efficient SMT solver (TACAS'08\/ETAPS'08)","author":"Moura Leonardo De","unstructured":"Leonardo De Moura and Nikolaj Bj\u00f8rner. 2008. Z3: an efficient SMT solver (TACAS'08\/ETAPS'08). Springer-Verlag, Berlin, Heidelberg, 337--340."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","unstructured":"Leonardo Mendon\u00e7a de Moura Soonho Kong Jeremy Avigad Floris van Doorn and Jakob von Raumer. 2015. The Lean Theorem Prover (System Description). In CADE. https:\/\/doi.org\/10.1007\/978-3-319-21401-6_26","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"e_1_3_2_1_8_1","volume-title":"VFP: A Virtual Switch Platform for Host Sdn in the Public Cloud. In NSDI.","author":"Firestone Daniel","year":"2017","unstructured":"Daniel Firestone. 2017. VFP: A Virtual Switch Platform for Host Sdn in the Public Cloud. In NSDI."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3387514.3405852"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3582016.3582036"},{"key":"e_1_3_2_1_11_1","volume-title":"SIMON: A Simple and Scalable Method for Sensing, Inference and Measurement in Data Center Networks. In NSDI.","author":"Geng Yilong","year":"2019","unstructured":"Yilong Geng, Shiyu Liu, Zi Yin, Ashish Naik, Balaji Prabhakar, Mendel Rosenblum, and Amin Vahdat. 2019. SIMON: A Simple and Scalable Method for Sensing, Inference and Measurement in Data Center Networks. In NSDI."},{"key":"e_1_3_2_1_12_1","volume-title":"Anderson","author":"Goyal Prateesh","year":"2022","unstructured":"Prateesh Goyal, Preey Shah, Kevin Zhao, Georgios Nikolaidis, Mohammad Alizadeh, and Thomas E. Anderson. 2022. Backpressure Flow Control. In NSDI."},{"key":"e_1_3_2_1_13_1","volume-title":"Programming by Examples - and its applications in Data Wrangling","author":"Gulwani Sumit","unstructured":"Sumit Gulwani. 2016. Programming by Examples - and its applications in Data Wrangling. In Dependable Software Systems Engineering, Javier Esparza, Orna Grumberg, and Salomon Sickert (Eds.). Vol. 45."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2934872.2934908"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3230543.3230555"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1400097.1400105"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3316482.3326344"},{"key":"e_1_3_2_1_18_1","unstructured":"VMWare Inc. 2023. VMware Container Networking with Antrea 1.7.0 Release Notes. https:\/\/docs.vmware.com\/en\/VMware-Container-Networking-with-Antrea\/1.7.0\/rn\/vmware-container-networking-with-antrea-170-release-notes.pdf"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","unstructured":"Grigoris Karvounarakis. 2009. Datalog. Springer US Boston MA 751--754. https:\/\/doi.org\/10.1007\/978-0-387-39940-9_968","DOI":"10.1007\/978-0-387-39940-9_968"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2785956.2787478"},{"key":"e_1_3_2_1_21_1","volume-title":"Swift: Delay is Simple and Effective for Congestion Control in the Datacenter. In SIGCOMM.","author":"Kumar Gautam","year":"2020","unstructured":"Gautam Kumar, Nandita Dukkipati, Keon Jang, Hassan M. G. Wassel, Xian Wu, Behnam Montazeri, Yaogong Wang, Kevin Springborn, Christopher Alfeld, Michael Ryan, David Wetherall, and Amin Vahdat. 2020. Swift: Delay is Simple and Effective for Congestion Control in the Datacenter. In SIGCOMM."},{"key":"e_1_3_2_1_22_1","volume-title":"Yan Zhuang, Fei Feng, Lingbo Tang, Zheng Cao, Ming Zhang, Frank Kelly, Mohammad Alizadeh, and Minlan Yu.","author":"Li Yuliang","year":"2019","unstructured":"Yuliang Li, Rui Miao, Hongqiang Harry Liu, Yan Zhuang, Fei Feng, Lingbo Tang, Zheng Cao, Ming Zhang, Frank Kelly, Mohammad Alizadeh, and Minlan Yu. 2019. HPCC: High Precision Congestion Control. In SIGCOMM."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","unstructured":"Michael Marty Marc de Kruijf Jacob Adriaens Christopher Alfeld Sean Bauer Carlo Contavalli Michael Dalton Nandita Dukkipati William C. Evans Steve Gribble Nicholas Kidd Roman Kononov Gautam Kumar Carl Mauer Emily Musick Lena Olson Erik Rubow Michael Ryan Kevin Springborn Paul Turner Valas Valancius Xi Wang and Amin Vahdat. 2019. Snap: A Microkernel Approach to Host Networking. In SOSP. https:\/\/doi.org\/10.1145\/3341301.3359657","DOI":"10.1145\/3341301.3359657"},{"key":"e_1_3_2_1_24_1","volume-title":"Nandita Dukkipati, Emily R. Blem, Hassan M. G. Wassel, Monia Ghobadi, Amin Vahdat, Yaogong Wang, David Wetherall, and David Zats.","author":"Mittal Radhika","year":"2015","unstructured":"Radhika Mittal, Vinh The Lam, Nandita Dukkipati, Emily R. Blem, Hassan M. G. Wassel, Monia Ghobadi, Amin Vahdat, Yaogong Wang, David Wetherall, and David Zats. 2015. TIMELY: RTT-based Congestion Control for the Datacenter. In SIGCOMM."},{"key":"e_1_3_2_1_25_1","unstructured":"Jeffrey C. Mogul Drago Goricanec Martin Pool Anees Shaikh Douglas Turk Bikash Koley and Xiaoxue Zhao. 2020. Experiences with Modeling Network Topologies at Multiple Levels of Abstraction. In NSDI."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","unstructured":"Srinivas Narayana Anirudh Sivaraman Vikram Nathan Prateesh Goyal Venkat Arun Mohammad Alizadeh Vimalkumar Jeyakumar and Changhoon Kim. 2017. Language-Directed Hardware Design for Network Performance Monitoring. In SIGCOMM. https:\/\/doi.org\/10.1145\/3098822.3098829","DOI":"10.1145\/3098822.3098829"},{"key":"e_1_3_2_1_27_1","unstructured":"OpenAI. 2024. How can I access GPT-4 GPT-4 Turbo and GPT-4o? https:\/\/help.openai.com\/en\/articles\/7102672-how-can-i-access-gpt-4-gpt-4-turbo-and-gpt-4o"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/AAI28216927"},{"key":"e_1_3_2_1_29_1","unstructured":"Perplexity AI. 2024. Perplexity. https:\/\/www.perplexity.ai. AI search and chat tool."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2619239.2626309"},{"key":"e_1_3_2_1_31_1","unstructured":"Ben Pfaff Justin Pettit Teemu Koponen Ethan J. Jackson Andy Zhou Jarno Rajahalme Jesse Gross Alex Wang Jonathan Stringer Pravin Shelar Keith Amidon and Mart\u00edn Casado. 2015. The Design and Implementation of Open VSwitch. In NSDI."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3387514.3405899"},{"key":"e_1_3_2_1_33_1","volume-title":"Robotron: Top-down Network Management at Facebook Scale. In SIGCOMM.","author":"Eric Sung Yu-Wei","year":"2016","unstructured":"Yu-Wei Eric Sung, Xiaozheng Tie, Starsky H.Y. Wong, and Hongyi Zeng. 2016. Robotron: Top-down Network Management at Facebook Scale. In SIGCOMM."},{"key":"e_1_3_2_1_34_1","unstructured":"Coq Team. [n.d.]. The Coq Proof Assistant. https:\/\/coq.inria.fr\/."},{"key":"e_1_3_2_1_35_1","volume-title":"Gemini: A Family of Highly Capable Multimodal Models. arXiv:2312.11805 [cs.CL] https:\/\/arxiv.org\/abs\/2312.11805","author":"Team Gemini","year":"2024","unstructured":"Gemini Team. 2024. Gemini: A Family of Highly Capable Multimodal Models. arXiv:2312.11805 [cs.CL] https:\/\/arxiv.org\/abs\/2312.11805"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"crossref","unstructured":"Michael Welzl and David Ros. 2011. RFC 6297: A Survey of Lower-than-Best-Effort Transport Protocols. (2011). https:\/\/www.rfc-editor.org\/rfc\/rfc6297","DOI":"10.17487\/rfc6297"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068411000494"},{"key":"e_1_3_2_1_38_1","unstructured":"Rafael J. Wysocki. 2017. Capacity Aware Scheduling in the Linux Kernel. https:\/\/www.kernel.org\/doc\/html\/latest\/scheduler\/sched-capacity.html"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3477132.3483569"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2999572.2999593"}],"event":{"name":"HotNets '24: The 23rd ACM Workshop on Hot Topics in Networks","location":"Irvine CA USA","acronym":"HotNets '24","sponsor":["SIGCOMM ACM Special Interest Group on Data Communication"]},"container-title":["Proceedings of the 23rd ACM Workshop on Hot Topics in Networks"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3696348.3696865","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3696348.3696865","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,22]],"date-time":"2025-08-22T16:06:04Z","timestamp":1755878764000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3696348.3696865"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,18]]},"references-count":40,"alternative-id":["10.1145\/3696348.3696865","10.1145\/3696348"],"URL":"https:\/\/doi.org\/10.1145\/3696348.3696865","relation":{},"subject":[],"published":{"date-parts":[[2024,11,18]]},"assertion":[{"value":"2024-11-18","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}