{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T07:24:39Z","timestamp":1774855479939,"version":"3.50.1"},"reference-count":45,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"3","license":[{"start":{"date-parts":[[2023,6,1]],"date-time":"2023-06-01T00:00:00Z","timestamp":1685577600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2023,6,1]],"date-time":"2023-06-01T00:00:00Z","timestamp":1685577600000},"content-version":"am","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2023,6,1]],"date-time":"2023-06-01T00:00:00Z","timestamp":1685577600000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2023,6,1]],"date-time":"2023-06-01T00:00:00Z","timestamp":1685577600000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CCF-2107429"],"award-info":[{"award-number":["CCF-2107429"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CCF-2107261"],"award-info":[{"award-number":["CCF-2107261"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CCF-2124431"],"award-info":[{"award-number":["CCF-2124431"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CNS-2104882"],"award-info":[{"award-number":["CNS-2104882"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CNS-2107147"],"award-info":[{"award-number":["CNS-2107147"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE\/ACM Trans. Networking"],"published-print":{"date-parts":[[2023,6]]},"DOI":"10.1109\/tnet.2022.3208551","type":"journal-article","created":{"date-parts":[[2022,9,29]],"date-time":"2022-09-29T19:39:53Z","timestamp":1664480393000},"page":"994-1009","source":"Crossref","is-referenced-by-count":4,"title":["Synthesizing Formal Network Specifications From Input-Output Examples"],"prefix":"10.1109","volume":"31","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8574-2120","authenticated-orcid":false,"given":"Haoxian","family":"Chen","sequence":"first","affiliation":[{"name":"University of Pennsylvania, Philadelphia, PA, USA"}]},{"given":"Chenyuan","family":"Wu","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, PA, USA"}]},{"given":"Andrew","family":"Zhao","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, PA, USA"}]},{"given":"Mukund","family":"Raghothaman","sequence":"additional","affiliation":[{"name":"University of Southern California, Los Angeles, CA, USA"}]},{"given":"Mayur","family":"Naik","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, PA, USA"}]},{"given":"Boon Thau","family":"Loo","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, PA, USA"}]}],"member":"263","reference":[{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1145\/3232565.3234462"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1145\/130385.130417"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43613-4_8"},{"key":"ref34","first-page":"1","article-title":"End-to-end differentiable proving","author":"rockt\u00e4schel","year":"2017","journal-title":"Proc Adv Neural Inf Process Syst (NeurIPS)"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2020\/673"},{"key":"ref37","first-page":"189","article-title":"BFT protocols under fire","author":"singh","year":"2008","journal-title":"Proc NSDI"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1145\/1322263.1322281"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1145\/3236024.3236034"},{"key":"ref31","first-page":"519","article-title":"Tierless programming and reasoning for software-defined networks","author":"nelson","year":"2014","journal-title":"Proc 11th USENIX Symp Netw Syst Design Implement (NSDI)"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(94)90035-3"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1145\/2934872.2934910"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1145\/3371130"},{"key":"ref10","first-page":"133","article-title":"Avenir: Managing data plane diversity with control plane synthesis","author":"campbell","year":"2021","journal-title":"Proc NSDI"},{"key":"ref32","year":"2020","journal-title":"POX"},{"key":"ref2","author":"abiteboul","year":"1994","journal-title":"Foundations of Databases The Logical Level"},{"key":"ref1","year":"2022","journal-title":"Netspec Synthesis Result Validation"},{"key":"ref17","first-page":"579","article-title":"NetComplete: Practical network-wide configuration synthesis with autocompletion","author":"el-hassany","year":"2018","journal-title":"Proc 15th USENIX Symp Netw Syst Design Implement (NSDI)"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009845"},{"key":"ref16","author":"cropper","year":"2016","journal-title":"Metagol System"},{"key":"ref38","year":"2020","journal-title":"Souffle"},{"key":"ref19","year":"2020","journal-title":"Floodlight"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1613\/jair.5714"},{"key":"ref24","article-title":"The ILASP system for inductive learning of answer set programs","author":"law","year":"2020","journal-title":"arXiv 2005 00904"},{"key":"ref23","first-page":"59","article-title":"Kinetic: Verifiable dynamic network control","author":"kim","year":"2015","journal-title":"Proc 12th USENIX Symp Netw Syst Design Implement (NSDI)"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1145\/1807167.1807234"},{"key":"ref26","first-page":"499","article-title":"Checking beliefs in dynamic networks","author":"lopes","year":"2015","journal-title":"Proc 12th USENIX Symp Netw Syst Design Implement (NSDI)"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1145\/1592761.1592785"},{"key":"ref20","first-page":"469","article-title":"A general approach to network configuration analysis","author":"fogel","year":"2015","journal-title":"Proc 12th USENIX Symp Netw Syst Design Implement (NSDI)"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062365"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2012.2187924"},{"key":"ref22","first-page":"49","article-title":"Veriflow: Verifying network-wide invariants in real time","author":"khurshid","year":"2013","journal-title":"Proc 10th USENIX Symp Netw Syst Design Implement (NSDI)"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1145\/2716281.2836119"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1145\/2034574.2034812"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1145\/2834050.2834112"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v35i7.16799"},{"key":"ref27","first-page":"100","article-title":"Differential testing for software","volume":"10","author":"mckeeman","year":"1998","journal-title":"Digit Tech J"},{"key":"ref29","year":"2019","journal-title":"Mininet"},{"key":"ref8","first-page":"969","article-title":"Config2Spec: Mining network specifications from network configurations","author":"birkner","year":"2020","journal-title":"Proc 17th USENIX Symp Netw Syst Design Implement (NSDI)"},{"key":"ref7","first-page":"328","article-title":"Don’t mind the gap: Bridging network-wide objectives and device-level configurations","author":"beckett","year":"2016","journal-title":"Proc ACM SIGCOMM Conf"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-14977-6_2"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_14"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1145\/1713254.1713261"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1145\/3098822.3098834"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594317"},{"key":"ref40","first-page":"61","article-title":"Declarative network verification","author":"wang","year":"2009","journal-title":"Proc Int Symp Practical Aspects Declarative Lang"}],"container-title":["IEEE\/ACM Transactions on Networking"],"original-title":[],"link":[{"URL":"https:\/\/ieeexplore.ieee.org\/ielam\/90\/10153803\/9905669-aam.pdf","content-type":"application\/pdf","content-version":"am","intended-application":"syndication"},{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/90\/10153803\/09905669.pdf?arnumber=9905669","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,7,3]],"date-time":"2023-07-03T18:42:38Z","timestamp":1688409758000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9905669\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6]]},"references-count":45,"journal-issue":{"issue":"3"},"URL":"https:\/\/doi.org\/10.1109\/tnet.2022.3208551","relation":{},"ISSN":["1063-6692","1558-2566"],"issn-type":[{"value":"1063-6692","type":"print"},{"value":"1558-2566","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,6]]}}}