{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,23]],"date-time":"2025-08-23T00:08:01Z","timestamp":1755907681503,"version":"3.44.0"},"publisher-location":"New York, NY, USA","reference-count":36,"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:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"NSF","award":["CNS-2312539,CCF-2107138"],"award-info":[{"award-number":["CNS-2312539,CCF-2107138"]}]},{"name":"NSERC","award":["Discovery"],"award-info":[{"award-number":["Discovery"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,11,18]]},"DOI":"10.1145\/3696348.3696854","type":"proceedings-article","created":{"date-parts":[[2024,11,11]],"date-time":"2024-11-11T00:20:52Z","timestamp":1731284452000},"page":"95-102","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Buffy: A Formal Language-Based Framework for Network Performance Analysis"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0004-7476-5791","authenticated-orcid":false,"given":"Amir","family":"Seyhani","sequence":"first","affiliation":[{"name":"University of Waterloo"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-2092-5147","authenticated-orcid":false,"given":"Junyi","family":"Zhao","sequence":"additional","affiliation":[{"name":"Princeton University"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6676-9400","authenticated-orcid":false,"given":"Aarti","family":"Gupta","sequence":"additional","affiliation":[{"name":"Princeton University"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3681-149X","authenticated-orcid":false,"given":"David","family":"Walker","sequence":"additional","affiliation":[{"name":"Princeton University"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5594-1110","authenticated-orcid":false,"given":"Mina Tahmasbi","family":"Arashloo","sequence":"additional","affiliation":[{"name":"University of Waterloo"}]}],"member":"320","published-online":{"date-parts":[[2024,11,18]]},"reference":[{"unstructured":"2023. FPerf Github Repository. https:\/\/github.com\/all-things-networking\/fperf\/tree\/main. Accessed: 2024--06.","key":"e_1_3_2_1_1_1"},{"unstructured":"2024. Buffy Github Repository. https:\/\/github.com\/all-things-networking\/hotnets24-buffy. Accessed: 2024--06.","key":"e_1_3_2_1_2_1"},{"key":"e_1_3_2_1_3_1","volume-title":"Ullman","author":"Aho Alfred V.","year":"1986","unstructured":"Alfred V. Aho, Ravi Sethi, and Jeffrey D. Ullman. 1986. Compilers: Principles, Techniques, and Tools. Addison-Wesley."},{"doi-asserted-by":"crossref","unstructured":"Mohammad Alizadeh Albert Greenberg David A Maltz Jitendra Padhye Parveen Patel Balaji Prabhakar Sudipta Sengupta and Murari Sridharan. 2010. Data center tcp (dctcp). In ACM SIGCOMM.","key":"e_1_3_2_1_4_1","DOI":"10.1145\/1851182.1851192"},{"doi-asserted-by":"crossref","unstructured":"Mohammad Alizadeh Shuang Yang Milad Sharif Sachin Katti Nick McKeown Balaji Prabhakar and Scott Shenker. 2013. pFabric: Minimal near-optimal datacenter transport. In ACM SIGCOMM.","key":"e_1_3_2_1_5_1","DOI":"10.1145\/2486001.2486031"},{"doi-asserted-by":"crossref","unstructured":"Rajeev Alur Rastislav Bod\u00edk Garvit Juniwal Milo M. K. Martin Mukund Raghothaman Sanjit A. Seshia Rishabh Singh Armando Solar-Lezama Emina Torlak and Abhishek Udupa. 2013. Syntaxguided synthesis. In FMCAD.","key":"e_1_3_2_1_6_1","DOI":"10.1109\/FMCAD.2013.6679385"},{"unstructured":"Carolyn Jane Anderson Nate Foster Arjun Guha Jean-Baptiste Jeannin Dexter Kozen Cole Schlesinger and David Walker. 2014. NetKAT: Semantic Foundations for Networks. In ACM SIGPLAN POPL.","key":"e_1_3_2_1_7_1"},{"unstructured":"Mina Tahmasbi Arashloo Ryan Beckett and Rachit Agarwal. 2023. Formal methods for network performance analysis. In USENIX NSDI.","key":"e_1_3_2_1_8_1"},{"key":"e_1_3_2_1_9_1","volume-title":"Ahmed Saeed, Mohammad Alizadeh, and Hari Balakrishnan.","author":"Arun Venkat","year":"2021","unstructured":"Venkat Arun, Mina Tahmasbi Arashloo, Ahmed Saeed, Mohammad Alizadeh, and Hari Balakrishnan. 2021. Toward formally verifying congestion control behavior. In ACM SIGCOMM."},{"unstructured":"Clark Barrett Pascal Fontaine and Cesare Tinelli. 2017. The SMT-LIB Standard: Version 2.6. Technical Report. Department of Computer Science The University of Iowa. Available at www.SMT-LIB.org.","key":"e_1_3_2_1_10_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_11_1","DOI":"10.1145\/3422604.3425930"},{"key":"e_1_3_2_1_12_1","volume-title":"Yaron Koral, Jennifer Rexford, Ori Rottenstreich, Steven A Monetti, and Tzuu-Yi Wang.","author":"Chen Xiaoqi","year":"2019","unstructured":"Xiaoqi Chen, Shir Landau Feibish, Yaron Koral, Jennifer Rexford, Ori Rottenstreich, Steven A Monetti, and Tzuu-Yi Wang. 2019. Fine-grained queue measurement in the data plane. In ACM CoNEXT."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_13_1","DOI":"10.1007\/978-3-540-24730-2_15"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_14_1","DOI":"10.1007\/978-3-540-78800-3_24"},{"doi-asserted-by":"crossref","unstructured":"Cormac Flanagan Rajeev Joshi and K. Rustan M. Leino. 2001. Annotation inference for modular checkers. Inform. Process. Lett. (2001).","key":"e_1_3_2_1_15_1","DOI":"10.1016\/S0020-0190(00)00196-4"},{"unstructured":"Ari Fogel Stanley Fung Luis Pedrosa Meg Walraed-Sullivan Ramesh Govindan Ratul Mahajan and Todd Millstein. 2015. A General Approach to Network Configuration Analysis. In USENIX NSDI.","key":"e_1_3_2_1_16_1"},{"key":"e_1_3_2_1_17_1","volume-title":"Probabilistic NetKAT. In European Symposium on Programming.","author":"Foster Nate","year":"2016","unstructured":"Nate Foster, Dexter Kozen, Konstantinos Mamouras, Mark Reitblatt, and Alexandra Silva. 2016. Probabilistic NetKAT. In European Symposium on Programming."},{"key":"e_1_3_2_1_18_1","volume-title":"Bayonet: Probabilistic inference for networks. In ACM SIGPLAN PLDI.","author":"Gehr Timon","year":"2018","unstructured":"Timon Gehr, Sasa Misailovic, Petar Tsankov, Laurent Vanbever, Pascal Wiesmann, and Martin Vechev. 2018. Bayonet: Probabilistic inference for networks. In ACM SIGPLAN PLDI."},{"key":"e_1_3_2_1_19_1","volume-title":"NV: An Intermediate Language for Verification of Network Control Planes. In ACM SIGPLAN PLDI.","author":"Giannarakis Nick","year":"2020","unstructured":"Nick Giannarakis, Devon Loehr, Ryan Beckett, and David Walker. 2020. NV: An Intermediate Language for Verification of Network Control Planes. In ACM SIGPLAN PLDI."},{"doi-asserted-by":"crossref","unstructured":"Mark Handley Costin Raiciu Alexandru Agache Andrei Voinescu Andrew W Moore Gianni Antichi and Marcin W\u00f3jcik. 2017. Re-architecting datacenter networks and stacks for low latency and high performance. In ACM SIGCOMM.","key":"e_1_3_2_1_20_1","DOI":"10.1145\/3098822.3098825"},{"doi-asserted-by":"crossref","unstructured":"Toke H\u00f8eiland-J\u00f8ergensen Paul McKenny Dave Taht Jim Gettys and Eric Dumazet. 2018. The Flow Queue CoDel packet scheduler and active queue management algorithm. RFC 8290. https:\/\/rfc-editor.org\/rfc\/rfc8290.txt","key":"e_1_3_2_1_21_1","DOI":"10.17487\/RFC8290"},{"unstructured":"Alex Horn Ali Kheradmand and Mukul Prasad. 2017. Delta-Net: Real-time network verification using atoms. In USENIX NSDI.","key":"e_1_3_2_1_22_1"},{"doi-asserted-by":"crossref","unstructured":"Karthick Jayaraman Nikolaj Bj\u00f8rner Jitu Padhye Amar Agrawal Ashish Bhargava Paul-Andre C Bissonnette et al. 2019. Validating datacenters at scale. In ACM SIGCOMM.","key":"e_1_3_2_1_23_1","DOI":"10.1145\/3341302.3342094"},{"key":"e_1_3_2_1_24_1","volume-title":"Quantitative network analysis. Technical report","author":"Juniwal Garvit","year":"2016","unstructured":"Garvit Juniwal, Nikolaj Bjorner, Ratul Mahajan, Sanjit Seshia, and George Varghese. 2016. Quantitative network analysis. Technical report (2016)."},{"unstructured":"Peyman Kazemian George Varghese and Nick McKeown. 2012. Header space analysis: Static checking for networks. In USENIX NSDI.","key":"e_1_3_2_1_25_1"},{"key":"e_1_3_2_1_26_1","volume-title":"Veriflow: Verifying network-wide invariants in real time. In USENIX NSDI.","author":"Khurshid Ahmed","year":"2013","unstructured":"Ahmed Khurshid, Xuan Zou, Wenxuan Zhou, Matthew Caesar, and P Brighten Godfrey. 2013. Veriflow: Verifying network-wide invariants in real time. In USENIX NSDI."},{"key":"e_1_3_2_1_27_1","volume-title":"SMT-based model checking for recursive programs. Formal Methods in System Design","author":"Komuravelli Anvesh","year":"2016","unstructured":"Anvesh Komuravelli, Arie Gurfinkel, and Sagar Chaki. 2016. SMT-based model checking for recursive programs. Formal Methods in System Design (2016)."},{"key":"e_1_3_2_1_28_1","volume-title":"International Conference on Principles of Distributed Systems (OPODIS).","author":"Larsen Kim G","year":"2017","unstructured":"Kim G Larsen, Stefan Schmid, and Bingtian Xue. 2017. WNetKAT: A weighted SDN programming and verification language. In International Conference on Principles of Distributed Systems (OPODIS)."},{"volume-title":"Network calculus: a theory of deterministic queuing systems for the internet","author":"Le Boudec Jean-Yves","unstructured":"Jean-Yves Le Boudec and Patrick Thiran. 2001. Network calculus: a theory of deterministic queuing systems for the internet. Springer.","key":"e_1_3_2_1_29_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_30_1","DOI":"10.1109\/MS.2017.4121212"},{"key":"e_1_3_2_1_31_1","volume-title":"Yan Zhuang, Fei Feng, Lingbo Tang, Zheng Cao, Ming Zhang, Frank Kelly, Mohammad Alizadeh, et al.","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, et al. 2019. HPCC: High precision congestion control. In ACM SIGCOMM."},{"unstructured":"Haohui Mai Ahmed Khurshid Rachit Agarwal Matthew Caesar P Brighten Godfrey and Samuel Talmadge King. 2011. Debugging the data plane with Anteater. In ACM SIGCOMM.","key":"e_1_3_2_1_32_1"},{"doi-asserted-by":"crossref","unstructured":"Anshuman Mohan Yunhe Liu Nate Foster Tobias Kapp\u00e9 and Dexter Kozen. 2023. Formal abstractions for packet scheduling. In ACM OOPSAL.","key":"e_1_3_2_1_33_1","DOI":"10.1145\/3622845"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_34_1","DOI":"10.1145\/2619239.2626309"},{"unstructured":"The P4.org Application Working Group. 2024. In-band Network Telemetry (INT) Dataplane Specification. https:\/\/p4.org\/p4-spec\/docs\/INT_v2_1.pdf.","key":"e_1_3_2_1_35_1"},{"volume-title":"SLA-verifier: Stateful and quantitative verification for service chaining","author":"Zhang Ying","unstructured":"Ying Zhang, Wenfei Wu, Sujata Banerjee, Joon-Myung Kang, and Mario A Sanchez. 2017. SLA-verifier: Stateful and quantitative verification for service chaining. In IEEE INFOCOM.","key":"e_1_3_2_1_36_1"}],"event":{"sponsor":["SIGCOMM ACM Special Interest Group on Data Communication"],"acronym":"HotNets '24","name":"HotNets '24: The 23rd ACM Workshop on Hot Topics in Networks","location":"Irvine CA USA"},"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.3696854","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3696348.3696854","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,22]],"date-time":"2025-08-22T16:08:30Z","timestamp":1755878910000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3696348.3696854"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,18]]},"references-count":36,"alternative-id":["10.1145\/3696348.3696854","10.1145\/3696348"],"URL":"https:\/\/doi.org\/10.1145\/3696348.3696854","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"}}]}}