{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,21]],"date-time":"2026-02-21T18:19:53Z","timestamp":1771697993101,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":63,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,11,28]],"date-time":"2023-11-28T00:00:00Z","timestamp":1701129600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100006374","name":"NSF (National Science Foundation)","doi-asserted-by":"publisher","award":["Grant CNS-2319442"],"award-info":[{"award-number":["Grant CNS-2319442"]}],"id":[{"id":"10.13039\/501100006374","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,11,28]]},"DOI":"10.1145\/3626111.3628188","type":"proceedings-article","created":{"date-parts":[[2023,11,13]],"date-time":"2023-11-13T12:11:20Z","timestamp":1699877480000},"page":"48-55","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Towards Integrating Formal Methods into ML-Based Systems for Networking"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-8184-9501","authenticated-orcid":false,"given":"Fengchen","family":"Gong","sequence":"first","affiliation":[{"name":"Princeton University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0231-2086","authenticated-orcid":false,"given":"Divya","family":"Raghunathan","sequence":"additional","affiliation":[{"name":"Princeton University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6676-9400","authenticated-orcid":false,"given":"Aarti","family":"Gupta","sequence":"additional","affiliation":[{"name":"Princeton University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0342-2631","authenticated-orcid":false,"given":"Maria","family":"Apostolaki","sequence":"additional","affiliation":[{"name":"Princeton University"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,11,28]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3387514.3405892"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3544216.3544252"},{"key":"e_1_3_2_1_3_1","volume-title":"FB: A flexible buffer management scheme for data center switches. arXiv preprint arXiv:2105.10553","author":"Apostolaki Maria","year":"2021","unstructured":"Maria Apostolaki, Vamsi Addanki, Manya Ghobadi, and Laurent Vanbever. 2021. FB: A flexible buffer management scheme for data center switches. arXiv preprint arXiv:2105.10553 (2021)."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-64322-8_7"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3482898.3483366"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3375235.3375237"},{"key":"e_1_3_2_1_7_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). 645--661."},{"key":"e_1_3_2_1_8_1","unstructured":"Arista. 2016. Arista LANZ Overview. https:\/\/arista.com\/assets\/data\/pdf\/Whitepapers\/Arista_LANZ_Overview_TechBulletin_0213.pdf."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3452296.3472912"},{"key":"e_1_3_2_1_10_1","volume-title":"Satisfiability modulo theories","author":"Barrett Clark","unstructured":"Clark Barrett and Cesare Tinelli. 2018. Satisfiability modulo theories. Springer."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563766.3564107"},{"key":"e_1_3_2_1_12_1","volume-title":"Proceedings of Tools and Algorithms for the Construction and Analysis of Systems. 3--25","author":"Henzinger Mathias Lechner Chatterjee Thomas A","year":"2023","unstructured":"Thomas A Henzinger Mathias Lechner Chatterjee, Krishnendu and Dorde Zikelic. 2023. A learner-verifier framework for neural network controllers and certificates of stochastic systems. In Proceedings of Tools and Algorithms for the Construction and Analysis of Systems. 3--25."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3359989.3365408"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/90.664262"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563766.3564104"},{"key":"e_1_3_2_1_17_1","volume-title":"Proceedings of The 4th Annual Learning for Dynamics and Control Conference (Proceedings of Machine Learning Research)","volume":"168","author":"Djeumou Franck","year":"2022","unstructured":"Franck Djeumou, Cyrus Neary, Eric Goubault, Sylvie Putot, and Ufuk Topcu. 2022. Neural Networks with Physics-Informed Architectures and Constraints for Dynamical Systems Modeling. In Proceedings of The 4th Annual Learning for Dynamics and Control Conference (Proceedings of Machine Learning Research), Vol. 168. PMLR, 263--277."},{"key":"e_1_3_2_1_18_1","volume-title":"Kaiming He, and Xiaoou Tang.","author":"Dong Chao","year":"2015","unstructured":"Chao Dong, Chen Change Loy, Kaiming He, and Xiaoou Tang. 2015. Image super-resolution using deep convolutional networks. IEEE transactions on pattern analysis and machine intelligence 38, 2 (2015), 295--307."},{"key":"e_1_3_2_1_19_1","volume-title":"15th USENIX Symposium on Networked Systems Design and Implementation (NSDI 18)","author":"Dong Mo","year":"2018","unstructured":"Mo Dong, Tong Meng, Doron Zarchy, Engin Arslan, Yossi Gilad, Brighten Godfrey, and Michael Schapira. 2018. PCC vivace: Online-learning congestion control. In 15th USENIX Symposium on Networked Systems Design and Implementation (NSDI 18). 343--356."},{"key":"e_1_3_2_1_20_1","volume-title":"15th USENIX Symposium on Networked Systems Design and Implementation (NSDI 18)","author":"El-Hassany Ahmed","year":"2018","unstructured":"Ahmed El-Hassany, Petar Tsankov, Laurent Vanbever, and Martin Vechev. 2018. Netcomplete: Practical network-wide configuration synthesis with autocompletion. In 15th USENIX Symposium on Networked Systems Design and Implementation (NSDI 18). 579--594."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3452296.3472936"},{"key":"e_1_3_2_1_22_1","volume-title":"James R. Davin, and Dr. Jeff D. Case.","author":"Fedor Mark","year":"1990","unstructured":"Mark Fedor, Martin Lee Schoffstall, James R. Davin, and Dr. Jeff D. Case. 1990. Simple Network Management Protocol (SNMP). RFC 1157. (May 1990)."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/90.251892"},{"key":"e_1_3_2_1_24_1","volume-title":"Inference and Measurement in Data Center Networks. In 16th USENIX Symposium on Networked Systems Design and Implementation (NSDI 19)","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 16th USENIX Symposium on Networked Systems Design and Implementation (NSDI 19). 549--564."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3365609.3365862"},{"key":"e_1_3_2_1_26_1","volume-title":"Blink: Fast Connectivity Recovery Entirely in the Data Plane. In 16th USENIX Symposium on Networked Systems Design and Implementation (NSDI 19)","author":"Holterbach Thomas","year":"2019","unstructured":"Thomas Holterbach, Edgar Costa Molero, Maria Apostolaki, Alberto Dainotti, Stefano Vissicchio, and Laurent Vanbever. 2019. Blink: Fast Connectivity Recovery Entirely in the Data Plane. In 16th USENIX Symposium on Networked Systems Design and Implementation (NSDI 19). USENIX Association, Boston, MA, 161--176."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2486001.2486012"},{"key":"e_1_3_2_1_28_1","volume-title":"CANE: A Cascade Control Approach for Network-Assisted Video QoE Management","author":"Hosseinzadeh Mehdi","year":"2023","unstructured":"Mehdi Hosseinzadeh, Karthick Shankar, Maria Apostolaki, Jay Ramachandran, Steven E Adams, Vyas Sekar, and Bruno Sinopoli. 2023. CANE: A Cascade Control Approach for Network-Assisted Video QoE Management. IEEE Transactions on Control Systems Technology (2023)."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563766.3564108"},{"key":"e_1_3_2_1_30_1","volume-title":"17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 20)","author":"Hsu Kuo-Feng","year":"2020","unstructured":"Kuo-Feng Hsu, Ryan Beckett, Ang Chen, Jennifer Rexford, and David Walker. 2020. Contra: A programmable system for performance-aware routing. In 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI 20). 701--721."},{"key":"e_1_3_2_1_31_1","volume-title":"Internet congestion control via deep reinforcement learning. arXiv preprint arXiv:1810.03259","author":"Jay Nathan","year":"2018","unstructured":"Nathan Jay, Noga H Rotman, P Godfrey, Michael Schapira, and Aviv Tamar. 2018. Internet congestion control via deep reinforcement learning. arXiv preprint arXiv:1810.03259 (2018)."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/POLICY.2009.32"},{"key":"e_1_3_2_1_33_1","volume-title":"David R Choffnes, Alan Mislove, and Cristina Nita-Rotaru.","author":"Jero Samuel","year":"2018","unstructured":"Samuel Jero, Md Endadul Hoque, David R Choffnes, Alan Mislove, and Cristina Nita-Rotaru. 2018. Automated Attack Discovery in TCP Congestion Control Using a Model-guided Approach.. In NDSS."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3445814.3446764"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1038\/s42254-021-00314-5"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563647.3563649"},{"key":"e_1_3_2_1_37_1","volume-title":"Formal Model-Driven Analysis of Resilience of GossipSub to Attacks from Misbehaving Peers. arXiv preprint arXiv:2212.05197","author":"Kumar Ankit","year":"2022","unstructured":"Ankit Kumar, Max von Hippel, Pete Manolios, and Cristina Nita-Rotaru. 2022. Formal Model-Driven Analysis of Resilience of GossipSub to Attacks from Misbehaving Peers. arXiv preprint arXiv:2212.05197 (2022)."},{"key":"e_1_3_2_1_38_1","volume-title":"Biologically-informed neural networks guide mechanistic modeling from sparse experimental data. PLoS computational biology 16, 12","author":"Lagergren John H","year":"2020","unstructured":"John H Lagergren, John T Nardini, Ruth E Baker, Matthew J Simpson, and Kevin B Flores. 2020. Biologically-informed neural networks guide mechanistic modeling from sparse experimental data. PLoS computational biology 16, 12 (2020), e1008462."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563766.3564109"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/CVPR.2017.19"},{"key":"e_1_3_2_1_41_1","volume-title":"Generating high-fidelity, synthetic time series datasets with doppelganger. arXiv preprint arXiv:1909.13403","author":"Lin Zinan","year":"2019","unstructured":"Zinan Lin, Alankar Jain, Chen Wang, Giulia Fanti, and Vyas Sekar. 2019. Generating high-fidelity, synthetic time series datasets with doppelganger. arXiv preprint arXiv:1909.13403 (2019)."},{"key":"e_1_3_2_1_42_1","volume-title":"Jaqen: A High-Performance Switch-Native Approach for Detecting and Mitigating Volumetric DDoS Attacks with Programmable Switches. In 30th USENIX Security Symposium (USENIX Security 21)","author":"Liu Zaoxing","year":"2021","unstructured":"Zaoxing Liu, Hun Namkung, Georgios Nikolaidis, Jeongkeun Lee, Changhoon Kim, Xin Jin, Vladimir Braverman, Minlan Yu, and Vyas Sekar. 2021. Jaqen: A High-Performance Switch-Native Approach for Detecting and Mitigating Volumetric DDoS Attacks with Programmable Switches. In 30th USENIX Security Symposium (USENIX Security 21). 3829--3846."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3387514.3405868"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371934.3371957"},{"key":"e_1_3_2_1_45_1","unstructured":"NS3. 2023. NS3 Network Simulator. https:\/\/www.nsnam.org\/."},{"key":"e_1_3_2_1_46_1","volume-title":"23rd International Symposium on Research in Attacks, Intrusions and Defenses (RAID","author":"Peterson Anthony","year":"2020","unstructured":"Anthony Peterson, Samuel Jero, Md Endadul Hoque, David R Choffnes, and Cristina Nita-Rotaru. 2020. aBBRate: Automating BBR Attack Exploration Using a Model-Based Approach. In 23rd International Symposium on Research in Attacks, Intrusions and Defenses (RAID 2020). 225--240."},{"key":"e_1_3_2_1_47_1","volume-title":"Carlo Tomasi, and Leonidas J Guibas","author":"Rubner Yossi","year":"2000","unstructured":"Yossi Rubner, Carlo Tomasi, and Leonidas J Guibas. 2000. The earth mover's distance as a metric for image retrieval. International journal of computer vision 40, 2 (2000), 99."},{"key":"e_1_3_2_1_48_1","unstructured":"Scikit-Learn. 2023. IterativeImputer\u00b6. https:\/\/scikit-learn.org\/stable\/modules\/generated\/sklearn.impute.IterativeImputer.html."},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3555050.3569129"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009845"},{"key":"e_1_3_2_1_51_1","volume-title":"Andrew Jaegle, S\u00e9bastien Racani\u00e8re, Aleksandar Botev, and Irina Higgins.","author":"Toth Peter","year":"2020","unstructured":"Peter Toth, Danilo Jimenez Rezende, Andrew Jaegle, S\u00e9bastien Racani\u00e8re, Aleksandar Botev, and Irina Higgins. 2020. Hamiltonian Generative Networks. (2020). arXiv:cs.LG\/1909.13789"},{"key":"e_1_3_2_1_52_1","volume-title":"\u0141 ukasz Kaiser, and Illia Polosukhin","author":"Vaswani Ashish","year":"2017","unstructured":"Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, \u0141 ukasz Kaiser, and Illia Polosukhin. 2017. Attention is All you Need. In Advances in Neural Information Processing Systems, I. Guyon, U. Von Luxburg, S. Bengio, H. Wallach, R. Fergus, S. Vishwanathan, and R. Garnett (Eds.), Vol. 30. Curran Associates, Inc. https:\/\/proceedings.neurips.cc\/paper_files\/paper\/2017\/file\/3f5ee243547dee91fbd053c1c4a845aa-Paper.pdf"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCVW54120.2021.00217"},{"key":"e_1_3_2_1_54_1","volume-title":"Proceedings of the European conference on computer vision (ECCV) workshops. 0--0.","author":"Wang Xintao","year":"2018","unstructured":"Xintao Wang, Ke Yu, Shixiang Wu, Jinjin Gu, Yihao Liu, Chao Dong, Yu Qiao, and Chen Change Loy. 2018. Esrgan: Enhanced super-resolution generative adversarial networks. In Proceedings of the European conference on computer vision (ECCV) workshops. 0--0."},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3375235.3375240"},{"key":"e_1_3_2_1_56_1","volume-title":"Proceedings of the 2019 Workshop on Buffer Sizing. 6.","author":"Woodruff Jackson","year":"2020","unstructured":"Jackson Woodruff, Andrew W Moore, and Noa Zilberman. 2020. Measuring Burstiness in Data Center Applications. In Proceedings of the 2019 Workshop on Buffer Sizing. 6."},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3603269.3604857"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3544216.3544248"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1109\/CVPR42600.2020.00328"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3131365.3131375"},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/3452296.3472926"},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1109\/CVPR.2018.00262"},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/2987550.2987585"}],"event":{"name":"HotNets '23: The 22nd ACM Workshop on Hot Topics in Networks","location":"Cambridge MA USA","acronym":"HotNets '23","sponsor":["SIGCOMM ACM Special Interest Group on Data Communication"]},"container-title":["Proceedings of the 22nd ACM Workshop on Hot Topics in Networks"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3626111.3628188","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3626111.3628188","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,22]],"date-time":"2025-08-22T19:39:11Z","timestamp":1755891551000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3626111.3628188"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,11,28]]},"references-count":63,"alternative-id":["10.1145\/3626111.3628188","10.1145\/3626111"],"URL":"https:\/\/doi.org\/10.1145\/3626111.3628188","relation":{},"subject":[],"published":{"date-parts":[[2023,11,28]]},"assertion":[{"value":"2023-11-28","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}