{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:14:13Z","timestamp":1750220053132,"version":"3.41.0"},"reference-count":62,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2023,1,9]],"date-time":"2023-01-09T00:00:00Z","timestamp":1673222400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["1837023, 2046071"],"award-info":[{"award-number":["1837023, 2046071"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,1,9]]},"abstract":"<jats:p>When managing wide-area networks, network architects must decide how to balance multiple conflicting metrics, and ensure fair allocations to competing traffic while prioritizing critical traffic. The state of practice poses challenges since architects must precisely encode their intent into formal optimization models using abstract notions such as utility functions, and ad-hoc manually tuned knobs. In this paper, we present the first effort to synthesize optimal network designs with indeterminate objectives using an interactive program-synthesis-based approach. We make three contributions. First, we present comparative synthesis, an interactive synthesis framework which produces near-optimal programs (network designs) through two kinds of queries (Validate and Compare), without an objective explicitly given. Second, we develop the first learning algorithm for comparative synthesis in which a voting-guided learner picks the most informative query in each iteration. We present theoretical analysis of the convergence rate of the algorithm. Third, we implemented Net10Q, a system based on our approach, and demonstrate its effectiveness on four real-world network case studies using black-box oracles and simulation experiments, as well as a pilot user study comprising network researchers and practitioners. Both theoretical and experimental results show the promise of our approach.<\/jats:p>","DOI":"10.1145\/3571197","type":"journal-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T21:58:14Z","timestamp":1673474294000},"page":"91-120","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Comparative Synthesis: Learning Near-Optimal Network Designs by Query"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9459-9813","authenticated-orcid":false,"given":"Yanjun","family":"Wang","sequence":"first","affiliation":[{"name":"Purdue University, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2228-4975","authenticated-orcid":false,"given":"Zixuan","family":"Li","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1877-5096","authenticated-orcid":false,"given":"Chuan","family":"Jiang","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9476-7349","authenticated-orcid":false,"given":"Xiaokang","family":"Qiu","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4825-4352","authenticated-orcid":false,"given":"Sanjay","family":"Rao","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}]}],"member":"320","published-online":{"date-parts":[[2023,1,11]]},"reference":[{"doi-asserted-by":"publisher","key":"e_1_2_2_1_1","DOI":"10.1145\/503272.503275"},{"doi-asserted-by":"publisher","key":"e_1_2_2_2_1","DOI":"10.1016\/j.tcs.2003.11.004"},{"doi-asserted-by":"publisher","key":"e_1_2_2_3_1","DOI":"10.1145\/3371110"},{"key":"e_1_2_2_4_1","volume-title":"Proceedings of 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI \u201920)","author":"Birkner R\u00fcdiger","year":"2020","unstructured":"R\u00fcdiger Birkner , Dana Drachsler-Cohen , Laurent Vanbever , and Martin Vechev . 2020 . Config2Spec: Mining Network Specifications from Network Configurations . In Proceedings of 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI \u201920) . R\u00fcdiger Birkner, Dana Drachsler-Cohen, Laurent Vanbever, and Martin Vechev. 2020. Config2Spec: Mining Network Specifications from Network Configurations. In Proceedings of 17th USENIX Symposium on Networked Systems Design and Implementation (NSDI \u201920)."},{"doi-asserted-by":"publisher","key":"e_1_2_2_5_1","DOI":"10.1145\/3341302.3342069"},{"doi-asserted-by":"publisher","key":"e_1_2_2_6_1","DOI":"10.1145\/2837614.2837666"},{"key":"e_1_2_2_7_1","volume-title":"Convex Optimization","author":"Boyd Stephen","year":"1833","unstructured":"Stephen Boyd and Lieven Vandenberghe . 2004. Convex Optimization . Cambridge University Press , USA. isbn:052 1833 787 Stephen Boyd and Lieven Vandenberghe. 2004. Convex Optimization. Cambridge University Press, USA. isbn:0521833787"},{"doi-asserted-by":"publisher","key":"e_1_2_2_8_1","DOI":"10.1145\/321892.321894"},{"unstructured":"Yiyang Chang Sanjay Rao and Mohit Tawarmalani. 2017. Robust Validation of Network Designs under Uncertain Demands and Failures. In 14^th USENIX Symposium on Networked Systems Design and Implementation (NSDI). 347\u2013362. \t\t\t\t  Yiyang Chang Sanjay Rao and Mohit Tawarmalani. 2017. Robust Validation of Network Designs under Uncertain Demands and Failures. In 14^th USENIX Symposium on Networked Systems Design and Implementation (NSDI). 347\u2013362.","key":"e_1_2_2_9_1"},{"doi-asserted-by":"publisher","key":"e_1_2_2_10_1","DOI":"10.1145\/2535838.2535859"},{"doi-asserted-by":"publisher","key":"e_1_2_2_11_1","DOI":"10.1109\/INFCOM.2012.6195833"},{"doi-asserted-by":"publisher","key":"e_1_2_2_12_1","DOI":"10.1007\/978-3-540-78800-3_24"},{"doi-asserted-by":"publisher","key":"e_1_2_2_13_1","DOI":"10.1007\/3-540-45014-9_1"},{"volume-title":"Synthesis with Abstract Examples","author":"Drachsler-Cohen Dana","unstructured":"Dana Drachsler-Cohen , Sharon Shoham , and Eran Yahav . 2017. Synthesis with Abstract Examples . In Computer Aided Verification, Rupak Majumdar and Viktor Kun\u010dak (Eds.). Springer International Publishing , Cham . 254\u2013278. isbn:978-3-319-63387-9 Dana Drachsler-Cohen, Sharon Shoham, and Eran Yahav. 2017. Synthesis with Abstract Examples. In Computer Aided Verification, Rupak Majumdar and Viktor Kun\u010dak (Eds.). Springer International Publishing, Cham. 254\u2013278. isbn:978-3-319-63387-9","key":"e_1_2_2_14_1"},{"doi-asserted-by":"publisher","key":"e_1_2_2_15_1","DOI":"10.1145\/3313831.3376442"},{"volume-title":"Network-Wide Configuration Synthesis","author":"El-Hassany Ahmed","unstructured":"Ahmed El-Hassany , Petar Tsankov , Laurent Vanbever , and Martin Vechev . 2017. Network-Wide Configuration Synthesis . In Computer Aided Verification, Rupak Majumdar and Viktor Kun\u010dak (Eds.). Springer International Publishing , Cham . 261\u2013281. isbn:978-3-319-63390-9 Ahmed El-Hassany, Petar Tsankov, Laurent Vanbever, and Martin Vechev. 2017. Network-Wide Configuration Synthesis. In Computer Aided Verification, Rupak Majumdar and Viktor Kun\u010dak (Eds.). Springer International Publishing, Cham. 261\u2013281. isbn:978-3-319-63390-9","key":"e_1_2_2_16_1"},{"key":"e_1_2_2_17_1","volume-title":"NetComplete: Practical Network-Wide Configuration Synthesis with Autocompletion. In 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) . USENIX Association, Renton, WA. 579\u2013594. isbn:978-1-93 1971-43-0 https:\/\/www.usenix.org\/conference\/nsdi18\/presentation\/el-hassany 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). USENIX Association, Renton, WA. 579\u2013594. isbn:978-1-931971-43-0 https:\/\/www.usenix.org\/conference\/nsdi18\/presentation\/el-hassany"},{"volume-title":"INFOCOM 2000. Nineteenth Annual Joint Conference of the IEEE Computer and Communications Societies. Proceedings. IEEE. 519\u2013528","author":"Fortz B.","unstructured":"B. Fortz and M. Thorup . 2000. Internet traffic engineering by optimizing OSPF weights . In INFOCOM 2000. Nineteenth Annual Joint Conference of the IEEE Computer and Communications Societies. Proceedings. IEEE. 519\u2013528 . B. Fortz and M. Thorup. 2000. Internet traffic engineering by optimizing OSPF weights. In INFOCOM 2000. Nineteenth Annual Joint Conference of the IEEE Computer and Communications Societies. Proceedings. IEEE. 519\u2013528.","key":"e_1_2_2_18_1"},{"doi-asserted-by":"publisher","key":"e_1_2_2_19_1","DOI":"10.1145\/3365609.3365858"},{"doi-asserted-by":"publisher","key":"e_1_2_2_20_1","DOI":"10.1007\/978-3-319-08867-9_5"},{"volume-title":"Numerical analysis: an introduction","author":"Gautschi Walter","unstructured":"Walter Gautschi . 1997. Numerical analysis: an introduction . Birkh\u00e4user , 215. Walter Gautschi. 1997. Numerical analysis: an introduction. Birkh\u00e4user, 215.","key":"e_1_2_2_21_1"},{"doi-asserted-by":"publisher","key":"e_1_2_2_22_1","DOI":"10.1109\/JSAC.2013.131208"},{"unstructured":"Sumit Gulwani Kunal Pathak Arjun Radhakrishna Ashish Tiwari and Abhishek Udupa. 2019. Quantitative Programming by Examples. arxiv:1909.05964. \t\t\t\t  Sumit Gulwani Kunal Pathak Arjun Radhakrishna Ashish Tiwari and Abhishek Udupa. 2019. Quantitative Programming by Examples. arxiv:1909.05964.","key":"e_1_2_2_23_1"},{"unstructured":"LLC Gurobi Optimization. 2020. Gurobi Optimizer Reference Manual. http:\/\/www.gurobi.com \t\t\t\t  LLC Gurobi Optimization. 2020. Gurobi Optimizer Reference Manual. http:\/\/www.gurobi.com","key":"e_1_2_2_24_1"},{"doi-asserted-by":"publisher","key":"e_1_2_2_25_1","DOI":"10.1145\/3230543.3230575"},{"doi-asserted-by":"publisher","key":"e_1_2_2_26_1","DOI":"10.1145\/2486001.2486012"},{"volume-title":"Syntax-Guided Synthesis with Quantitative Syntactic Objectives","author":"Hu Qinheping","unstructured":"Qinheping Hu and Loris D\u2019Antoni . 2018. Syntax-Guided Synthesis with Quantitative Syntactic Objectives . In Computer Aided Verification, Hana Chockler and Georg Weissenbacher (Eds.). Springer International Publishing , Cham . 386\u2013403. isbn:978-3-319-96145-3 Qinheping Hu and Loris D\u2019Antoni. 2018. Syntax-Guided Synthesis with Quantitative Syntactic Objectives. In Computer Aided Verification, Hana Chockler and Georg Weissenbacher (Eds.). Springer International Publishing, Cham. 386\u2013403. isbn:978-3-319-96145-3","key":"e_1_2_2_27_1"},{"doi-asserted-by":"publisher","key":"e_1_2_2_28_1","DOI":"10.1145\/2534169.2486019"},{"doi-asserted-by":"publisher","key":"e_1_2_2_29_1","DOI":"10.1145\/1806799.1806833"},{"doi-asserted-by":"publisher","key":"e_1_2_2_30_1","DOI":"10.1007\/s00236-017-0294-5"},{"doi-asserted-by":"publisher","key":"e_1_2_2_31_1","DOI":"10.1145\/3385412.3386025"},{"doi-asserted-by":"publisher","key":"e_1_2_2_32_1","DOI":"10.1145\/3387514.3405858"},{"doi-asserted-by":"publisher","key":"e_1_2_2_33_1","DOI":"10.1109\/JSAC.2011.111002"},{"doi-asserted-by":"publisher","key":"e_1_2_2_34_1","DOI":"10.1145\/2829988.2787478"},{"doi-asserted-by":"publisher","key":"e_1_2_2_35_1","DOI":"10.1145\/3232755.3232781"},{"doi-asserted-by":"publisher","key":"e_1_2_2_36_1","DOI":"10.1145\/2535838.2535857"},{"doi-asserted-by":"publisher","key":"e_1_2_2_37_1","DOI":"10.1145\/2619239.2626314"},{"doi-asserted-by":"publisher","key":"e_1_2_2_38_1","DOI":"10.1145\/2807442.2807459"},{"doi-asserted-by":"publisher","key":"e_1_2_2_39_1","DOI":"10.1145\/2908080.2908097"},{"doi-asserted-by":"publisher","key":"e_1_2_2_40_1","DOI":"10.1145\/2737924.2737980"},{"doi-asserted-by":"publisher","key":"e_1_2_2_41_1","DOI":"10.1007\/978-3-540-88908-3_2"},{"doi-asserted-by":"publisher","key":"e_1_2_2_42_1","DOI":"10.1145\/3180155.3180189"},{"key":"e_1_2_2_43_1","volume-title":"14th USENIX Symposium on Networked Systems Design and Implementation (NSDI 17)","author":"Ryzhyk Leonid","year":"2017","unstructured":"Leonid Ryzhyk , Nikolaj Bj\u00f8rner , Marco Canini , Jean-Baptiste Jeannin , Cole Schlesinger , Douglas B. Terry , and George Varghese . 2017 . Correct by Construction Networks Using Stepwise Refinement . In 14th USENIX Symposium on Networked Systems Design and Implementation (NSDI 17) . USENIX Association, Boston, MA. 683\u2013698. isbn:978-1-93 1971-37-9 https:\/\/www.usenix.org\/conference\/nsdi17\/technical-sessions\/presentation\/ryzhyk Leonid Ryzhyk, Nikolaj Bj\u00f8rner, Marco Canini, Jean-Baptiste Jeannin, Cole Schlesinger, Douglas B. Terry, and George Varghese. 2017. Correct by Construction Networks Using Stepwise Refinement. In 14th USENIX Symposium on Networked Systems Design and Implementation (NSDI 17). USENIX Association, Boston, MA. 683\u2013698. isbn:978-1-931971-37-9 https:\/\/www.usenix.org\/conference\/nsdi17\/technical-sessions\/presentation\/ryzhyk"},{"doi-asserted-by":"publisher","key":"e_1_2_2_44_1","DOI":"10.1145\/2774993.2775006"},{"doi-asserted-by":"publisher","key":"e_1_2_2_45_1","DOI":"10.1145\/2451116.2451150"},{"doi-asserted-by":"publisher","key":"e_1_2_2_46_1","DOI":"10.1145\/2594291.2594302"},{"doi-asserted-by":"publisher","key":"e_1_2_2_47_1","DOI":"10.2200\/S00429ED1V01Y201207AIM018"},{"doi-asserted-by":"publisher","key":"e_1_2_2_48_1","DOI":"10.1145\/130385.130417"},{"key":"e_1_2_2_49_1","volume-title":"Boon Thau Loo, and Rajeev Alur","author":"Shi Lei","year":"2021","unstructured":"Lei Shi , Yahui Li , Boon Thau Loo, and Rajeev Alur . 2021 . Network Traffic Classification by Program Synthesis. In Tools and Algorithms for the Construction and Analysis of Systems, Jan Friso Groote and Kim Guldstrand Larsen (Eds.). Springer International Publishing , Cham. 430\u2013448. isbn:978-3-030-72016-2 Lei Shi, Yahui Li, Boon Thau Loo, and Rajeev Alur. 2021. Network Traffic Classification by Program Synthesis. In Tools and Algorithms for the Construction and Analysis of Systems, Jan Friso Groote and Kim Guldstrand Larsen (Eds.). Springer International Publishing, Cham. 430\u2013448. isbn:978-3-030-72016-2"},{"doi-asserted-by":"publisher","key":"e_1_2_2_50_1","DOI":"10.1145\/2934872.2934900"},{"unstructured":"Armando Solar-Lezama. 2016. The Sketch Programmers Manual. Version 1.7.2 \t\t\t\t  Armando Solar-Lezama. 2016. The Sketch Programmers Manual. Version 1.7.2","key":"e_1_2_2_51_1"},{"doi-asserted-by":"crossref","unstructured":"Armando Solar-Lezama Liviu Tancau Rastislav Bodik Sanjit Seshia and Vijay Saraswat. 2006. Combinatorial sketching for finite programs. In ASPLOS\u201906. ACM 404\u2013415. \t\t\t\t  Armando Solar-Lezama Liviu Tancau Rastislav Bodik Sanjit Seshia and Vijay Saraswat. 2006. Combinatorial sketching for finite programs. In ASPLOS\u201906. ACM 404\u2013415.","key":"e_1_2_2_52_1","DOI":"10.1145\/1168918.1168907"},{"doi-asserted-by":"publisher","key":"e_1_2_2_53_1","DOI":"10.1145\/2674005.2674989"},{"doi-asserted-by":"publisher","key":"e_1_2_2_54_1","DOI":"10.1007\/978-0-8176-8216-3"},{"doi-asserted-by":"publisher","key":"e_1_2_2_55_1","DOI":"10.1145\/3387514.3405900"},{"doi-asserted-by":"publisher","key":"e_1_2_2_56_1","DOI":"10.1145\/3385412.3385976"},{"doi-asserted-by":"publisher","key":"e_1_2_2_57_1","DOI":"10.1145\/3009837.3009845"},{"doi-asserted-by":"publisher","key":"e_1_2_2_58_1","DOI":"10.1145\/2038642.2038666"},{"doi-asserted-by":"publisher","key":"e_1_2_2_59_1","DOI":"10.1109\/JSAC.2009.090409"},{"doi-asserted-by":"publisher","key":"e_1_2_2_60_1","DOI":"10.1145\/3365609.3365861"},{"doi-asserted-by":"publisher","key":"e_1_2_2_61_1","DOI":"10.1145\/1851182.1851218"},{"doi-asserted-by":"publisher","key":"e_1_2_2_62_1","DOI":"10.1145\/2716281.2836119"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571197","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3571197","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:08:21Z","timestamp":1750183701000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571197"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,9]]},"references-count":62,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2023,1,9]]}},"alternative-id":["10.1145\/3571197"],"URL":"https:\/\/doi.org\/10.1145\/3571197","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2023,1,9]]},"assertion":[{"value":"2023-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}