{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,8]],"date-time":"2026-04-08T20:41:42Z","timestamp":1775680902376,"version":"3.50.1"},"reference-count":183,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"1","license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/OAPA.html"}],"funder":[{"name":"National High Technology Research and Development Program of China 863 Program","award":["2015AA016105"],"award-info":[{"award-number":["2015AA016105"]}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61402253"],"award-info":[{"award-number":["61402253"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Commun. Surv. Tutorials"],"published-print":{"date-parts":[[2019]]},"DOI":"10.1109\/comst.2018.2868050","type":"journal-article","created":{"date-parts":[[2018,8,31]],"date-time":"2018-08-31T18:40:11Z","timestamp":1535740811000},"page":"940-969","source":"Crossref","is-referenced-by-count":42,"title":["A Survey on Network Verification and Testing With Formal Methods: Approaches and Challenges"],"prefix":"10.1109","volume":"21","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7094-4053","authenticated-orcid":false,"given":"Yahui","family":"Li","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xia","family":"Yin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6587-820X","authenticated-orcid":false,"given":"Zhiliang","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jiangyuan","family":"Yao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xingang","family":"Shi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jianping","family":"Wu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Han","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Qing","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref170","doi-asserted-by":"crossref","first-page":"777","DOI":"10.1093\/genetics\/159.2.777","article-title":"Synergistic derepression of gibberellin signaling by removing RGA and GAI function in arabidopsis thaliana","volume":"159","author":"dill","year":"2001","journal-title":"Genetics"},{"key":"ref172","doi-asserted-by":"publisher","DOI":"10.1145\/1837274.1837466"},{"key":"ref171","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"ref174","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44585-4_9"},{"key":"ref173","doi-asserted-by":"publisher","DOI":"10.1145\/1644893.1644909"},{"key":"ref176","doi-asserted-by":"publisher","DOI":"10.1145\/1868447.1868466"},{"key":"ref175","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4899-7637-6_11"},{"key":"ref178","first-page":"63","article-title":"Requirements for traffic engineering over MPLS","volume":"10","author":"awduche","year":"1999","journal-title":"Journal of evidence-based social work"},{"key":"ref177","year":"2016","journal-title":"BuDDy A BDD package"},{"key":"ref168","doi-asserted-by":"publisher","DOI":"10.1145\/2785956.2790038"},{"key":"ref169","doi-asserted-by":"publisher","DOI":"10.1145\/2619239.2626313"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"ref38","first-page":"995","article-title":"Temporal and modal logic","author":"emerson","year":"1990","journal-title":"Handbook of Theoretical Computer Science Volume B Formal Models and Semantics (B)"},{"key":"ref33","first-page":"1","article-title":"The birth of model checking","author":"clarke","year":"2008","journal-title":"25 Years of Model Checking—History Achievements Perspectives"},{"key":"ref32","author":"baier","year":"2008","journal-title":"Principles of Model Checking"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"ref30","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s100090050010","article-title":"UPPAAL in a nutshell","volume":"1","author":"larsen","year":"1997","journal-title":"Int J Softw Tools Technol Transfer"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1145\/1989323.1989456"},{"key":"ref36","first-page":"2829","article-title":"Artificial intelligence: A modern approach","volume":"263","author":"norvig","year":"2003","journal-title":"Applied Mechanics and Material"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1109\/5.533956"},{"key":"ref34","author":"marker","year":"2002","journal-title":"Model Theory An Introduction"},{"key":"ref181","doi-asserted-by":"publisher","DOI":"10.1145\/2619239.2626335"},{"key":"ref180","first-page":"25","article-title":"Differential provenance: Better network diagnostics with reference events","author":"chen","year":"2015","journal-title":"Proc 11th ACM Workshop Hot Topics Netw"},{"key":"ref183","doi-asserted-by":"publisher","DOI":"10.21236\/ADA419626"},{"key":"ref182","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1145\/2934872.2934910","article-title":"The good, the bad, and the differences: Better network diagnostics with differential provenance","author":"chen","year":"2016","journal-title":"Proc ACM SIGCOMM Conf"},{"key":"ref28","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","article-title":"NuSMV 2: An OpenSource tool for symbolic model checking","author":"cimatti","year":"2002","journal-title":"Proc 14th Int Conf Comput -Aided Verification (CAV)"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"ref179","first-page":"29","article-title":"OFRewind: Enabling record and replay troubleshooting for networks","author":"wundsam","year":"2011","journal-title":"Proc of USENIX Tech Conf USENIX"},{"key":"ref29","author":"jackson","year":"2006","journal-title":"Software Abstractions–Logic Language and Analysis"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.17487\/rfc2474"},{"key":"ref22","doi-asserted-by":"crossref","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","article-title":"PRISM 4.0: Verification of probabilistic real-time systems","author":"kwiatkowska","year":"2011","journal-title":"Proc 23rd Int Conf Comput -Aided Verification (CAV)"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1145\/1355734.1355746"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.17487\/rfc1654"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1109\/MNET.1998.752629"},{"key":"ref101","doi-asserted-by":"publisher","DOI":"10.1109\/MASCOTS.2017.20"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/1384609.1384625"},{"key":"ref100","doi-asserted-by":"publisher","DOI":"10.1145\/2680821.2680828"},{"key":"ref25","first-page":"127","article-title":"A NICE way to test openflow applications","author":"canini","year":"2012","journal-title":"Proc USENIX Symp Netw Syst Design Implem (NSDI)"},{"key":"ref50","first-page":"519","article-title":"Tierless programming and reasoning for software-defined networks","author":"nelson","year":"2014","journal-title":"Proc USENIX\/ACM Symp Netw Syst Design Implement"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1145\/1866898.1866905"},{"key":"ref154","doi-asserted-by":"publisher","DOI":"10.1007\/s11432-008-0156-4"},{"key":"ref153","doi-asserted-by":"publisher","DOI":"10.1109\/NFV-SDN.2016.7919488"},{"key":"ref156","first-page":"154","article-title":"Counterexample-guided abstraction refinement","author":"clarke","year":"2000","journal-title":"Proc 12th Int Conf Comput -Aided Verification (CAV)"},{"key":"ref155","doi-asserted-by":"publisher","DOI":"10.1145\/2620728.2620751"},{"key":"ref150","doi-asserted-by":"publisher","DOI":"10.1109\/EWSDN.2012.21"},{"key":"ref152","doi-asserted-by":"publisher","DOI":"10.1145\/3005745.3005754"},{"key":"ref151","doi-asserted-by":"crossref","first-page":"347","DOI":"10.1007\/978-3-319-15509-8_26","article-title":"What you need to know about SDN flow tables","author":"kuzniar","year":"2015","journal-title":"Proc 17th Int Conf Passive Active Meas (PAM)"},{"key":"ref146","year":"2015","journal-title":"OpenFlow Switch Specification"},{"key":"ref147","doi-asserted-by":"publisher","DOI":"10.1109\/ICNP.2014.37"},{"key":"ref148","year":"2014","journal-title":"OFTest-Validating OpenFlow Swtiches"},{"key":"ref149","first-page":"85","article-title":"OFLOPS: An open framework for OpenFlow switch evaluation","author":"rotsos","year":"2012","journal-title":"Proc 13th Int Conf MEMS"},{"key":"ref59","first-page":"1","article-title":"Scalable testing of context-dependent policies over stateful data planes with armstrong","author":"fayaz","year":"2015","journal-title":"CoRR vol abs\/1505 03356"},{"key":"ref58","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535862"},{"key":"ref57","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462178"},{"key":"ref56","author":"bertot","year":"2004","journal-title":"Interactive Theorem Proving and Program Development—Coq’Art The Calculus of Inductive Constructions (Texts in Theoretical Computer Science An EATCS Series)"},{"key":"ref55","author":"nipkow","year":"2002","journal-title":"Isabelle\/HOL - A Proof Assistant for Higher-order Logic (LNCS 2283)"},{"key":"ref54","doi-asserted-by":"publisher","DOI":"10.1145\/2666356.2594317"},{"key":"ref53","doi-asserted-by":"crossref","first-page":"390","DOI":"10.1007\/3-540-61474-5_86","article-title":"The murphi verification system","author":"dill","year":"1996","journal-title":"Proc Int Conf Comput -Aided Verification"},{"key":"ref52","first-page":"101","article-title":"Software dataplane verification","author":"dobrescu","year":"2014","journal-title":"Proc USENIX Symp Netw Syst Design Implem (NSDI)"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011276507260"},{"key":"ref167","first-page":"6","article-title":"Destroying networks for fun (and profit)","author":"shelly","year":"2015","journal-title":"Proc 14th ACM Workshop Hot Topics Netw"},{"key":"ref166","doi-asserted-by":"publisher","DOI":"10.1109\/NOMS.2014.6838225"},{"key":"ref165","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"ref164","doi-asserted-by":"publisher","DOI":"10.1145\/2619239.2626304"},{"key":"ref163","doi-asserted-by":"publisher","DOI":"10.1109\/REAL.1996.563702"},{"key":"ref162","doi-asserted-by":"crossref","first-page":"232","DOI":"10.1007\/BFb0020949","article-title":"UPPAAL—A tool suite for automatic verification of real-time systems","author":"bengtsson","year":"1996","journal-title":"Proc DIMACS Workshop on Verification and Control of Hybrid Systems"},{"key":"ref161","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"ref160","first-page":"165","article-title":"Systematically exploring the behavior of control programs","author":"croft","year":"2015","journal-title":"Proc USENIX Annu Tech Conf USENIX ATC"},{"key":"ref4","year":"2012","journal-title":"Software-Defined Networking The New Norm for Networks"},{"key":"ref3","year":"2004","journal-title":"traceroute"},{"key":"ref6","first-page":"113","article-title":"Header space analysis: Static checking for networks","author":"kazemian","year":"2012","journal-title":"Proc USENIX Symp Netw Syst Design Implem (NSDI)"},{"key":"ref5","author":"varghese","year":"2015","journal-title":"Vision for Network Design Automation and Network Verification"},{"key":"ref159","first-page":"110","article-title":"Dynamic partial-order reduction for model checking software","author":"flanagan","year":"2005","journal-title":"Proc ACM SIGPLAN-SIGACT Symp Principles Program Lang"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/581771.581775"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2014.6987609"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/COMST.2002.5341329"},{"key":"ref157","doi-asserted-by":"publisher","DOI":"10.1145\/2025113.2025151"},{"key":"ref158","doi-asserted-by":"publisher","DOI":"10.1109\/APNOMS.2014.6996558"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1145\/2018436.2018470"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1145\/222124.222148"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36384-X_5"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679403"},{"key":"ref47","first-page":"39","author":"singh","year":"2008","journal-title":"Model-Checking Based Verification for Hardware Designs Specified Using Bluespec System Verilog"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"ref41","doi-asserted-by":"crossref","first-page":"419","DOI":"10.1007\/3-540-61474-5_93","article-title":"Symbolic model checking","author":"clarke","year":"1996","journal-title":"Proc 8th Int Conf Comput -Aided Verification (CAV)"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.21236\/ADA360973"},{"key":"ref43","first-page":"161","article-title":"The SMV system","volume":"38","author":"mcmillan","year":"1992","journal-title":"Symbolic Model Checking"},{"key":"ref127","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-84882-828-5","author":"kalmanek","year":"2010","journal-title":"Guide to Reliable Internet Services and Applications"},{"key":"ref126","doi-asserted-by":"publisher","DOI":"10.1109\/INFCOM.2004.1354680"},{"key":"ref125","year":"2016","journal-title":"The intel intrinsics guide"},{"key":"ref124","doi-asserted-by":"publisher","DOI":"10.1049\/ip-e.1981.0052"},{"key":"ref73","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71209-1_49"},{"key":"ref72","first-page":"502","article-title":"MiniSat: A SAT solver with conflict-clause minimization","author":"een","year":"2005","journal-title":"Proc Int Conf Theory and Appl Satisfiability Testing"},{"key":"ref129","doi-asserted-by":"publisher","DOI":"10.1145\/2461446.2461461"},{"key":"ref71","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0247-6"},{"key":"ref128","first-page":"1","article-title":"The margrave tool for firewall analysis","author":"nelson","year":"2010","journal-title":"Proc Int Conf Large Install Syst Admin"},{"key":"ref70","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","article-title":"Z3: An efficient SMT solver","author":"de moura","year":"2008","journal-title":"Proc 14th Int Conf Tools Algorithms Construct Anal Syst (TACAS)"},{"key":"ref76","doi-asserted-by":"publisher","DOI":"10.1145\/2491185.2491187"},{"key":"ref130","doi-asserted-by":"publisher","DOI":"10.1109\/IC2E.2014.72"},{"key":"ref77","doi-asserted-by":"publisher","DOI":"10.1145\/2408776.2408795"},{"key":"ref74","author":"chang","year":"1973","journal-title":"Symbolic Logic and Mechanical Theorem Proving (Computer Science Classics)"},{"key":"ref75","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"ref133","first-page":"1","article-title":"Proof-based verification of software defined networks","author":"chen","year":"2014","journal-title":"Open Networking Summit (ONS) Research Track"},{"key":"ref134","first-page":"1","article-title":"Logic programming for software-defined networks","author":"katta","year":"2013","journal-title":"Proc Workshop Cross"},{"key":"ref131","doi-asserted-by":"publisher","DOI":"10.1145\/2342356.2342427"},{"key":"ref78","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"ref132","first-page":"1","article-title":"Composing software defined networks","author":"monsanto","year":"2013","journal-title":"Proc USENIX Symp Netw Syst Design Implem (NSDI)"},{"key":"ref79","first-page":"275","article-title":"Buzz: Testing context-dependent policies in stateful networks","author":"fayaz","year":"2016","journal-title":"Proc USENIX Symp Netw Syst Design Implem (NSDI)"},{"key":"ref136","doi-asserted-by":"publisher","DOI":"10.1145\/2486001.2486030"},{"key":"ref135","doi-asserted-by":"publisher","DOI":"10.1109\/MCOM.2013.6461197"},{"key":"ref138","doi-asserted-by":"publisher","DOI":"10.1145\/2716281.2836117"},{"key":"ref137","doi-asserted-by":"publisher","DOI":"10.1145\/2491185.2491201"},{"key":"ref60","first-page":"209","article-title":"KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs","author":"cadar","year":"2008","journal-title":"Proc 5th USENIX Conf Operating Syst Design Implementation"},{"key":"ref139","doi-asserted-by":"publisher","DOI":"10.1145\/2674005.2675006"},{"key":"ref62","doi-asserted-by":"crossref","first-page":"496","DOI":"10.1007\/978-3-319-02444-8_43","article-title":"SAT based verification of network data planes","volume":"8172","author":"zhang","year":"2013","journal-title":"Automated Technology for Verification and Analysis"},{"key":"ref61","doi-asserted-by":"publisher","DOI":"10.1145\/2934872.2934881"},{"key":"ref63","doi-asserted-by":"publisher","DOI":"10.1109\/ICC.2013.6654813"},{"key":"ref64","first-page":"1","article-title":"Yices 1.0: An efficient SMT solver","volume":"54","author":"de moura","year":"2006","journal-title":"The Satisfiability Modulo Theories Competition"},{"key":"ref140","doi-asserted-by":"publisher","DOI":"10.1109\/INFOCOM.2016.7524333"},{"key":"ref65","first-page":"499","article-title":"Checking beliefs in dynamic networks","author":"lopes","year":"2015","journal-title":"Proc USENIX\/ACM Symp Netw Syst Design Implement"},{"key":"ref141","first-page":"71","article-title":"I know what your packet did last hop: Using packet histories to troubleshoot networks","author":"handigol","year":"2014","journal-title":"Proc USENIX\/ACM Symp Netw Syst Design Implement"},{"key":"ref66","author":"gordon","year":"1987","journal-title":"HOL A proof generating system for higher-order logic"},{"key":"ref142","article-title":"Measuring and troubleshooting large operational multipath networks with gray box testing","author":"zeng","year":"2015"},{"key":"ref67","doi-asserted-by":"publisher","DOI":"10.1145\/2093548.2093564"},{"key":"ref143","doi-asserted-by":"publisher","DOI":"10.1145\/2785956.2787496"},{"key":"ref68","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/978-3-540-79124-9_10","article-title":"Pex—White box test generation for.NET","author":"tillmann","year":"2008","journal-title":"Proc 2nd Int Conf Tests Proofs (TAP)"},{"key":"ref144","doi-asserted-by":"publisher","DOI":"10.1145\/2413176.2413207"},{"key":"ref2","author":"muuss","year":"1983","journal-title":"The Story of the PING Program"},{"key":"ref69","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-013-0122-2"},{"key":"ref145","doi-asserted-by":"publisher","DOI":"10.1145\/2486001.2491711"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/2413176.2413205"},{"key":"ref109","doi-asserted-by":"publisher","DOI":"10.1145\/2342441.2342452"},{"key":"ref95","doi-asserted-by":"publisher","DOI":"10.1145\/2934872.2934876"},{"key":"ref108","first-page":"735","article-title":"Delta-net: Real-time network verification using atoms","author":"horn","year":"2017","journal-title":"Proc USENIX Symp Netw Syst Design Implem (NSDI)"},{"key":"ref94","first-page":"469","article-title":"A general approach to network configuration analysis","author":"fogel","year":"2015","journal-title":"Proc USENIX Symp Netw Syst Design Implem (NSDI)"},{"key":"ref107","first-page":"99","article-title":"Real time network policy checking using header space analysis","author":"kazemian","year":"2013","journal-title":"Proc USENIX\/ACM Symp Netw Syst Design Implement"},{"key":"ref93","doi-asserted-by":"publisher","DOI":"10.1109\/INFOCOM.2017.8057041"},{"key":"ref106","first-page":"69","article-title":"Scaling network verification using symmetry and surgery","author":"plotkin","year":"2014","journal-title":"Proc ACM PLDI"},{"key":"ref92","article-title":"Verifying isolation properties in the presence of middleboxes","volume":"abs 1409 7687","author":"panda","year":"2014","journal-title":"CoRR"},{"key":"ref105","first-page":"87","article-title":"Libra: Divide and conquer to verify forwarding tables in huge networks","author":"zeng","year":"2014","journal-title":"Proc USENIX NSDI"},{"key":"ref91","doi-asserted-by":"publisher","DOI":"10.1145\/2377677.2377766"},{"key":"ref104","doi-asserted-by":"publisher","DOI":"10.1109\/ICNP.2013.6733614"},{"key":"ref90","first-page":"199","article-title":"FIREMAN: A toolkit for firewall modeling and analysis","author":"yuan","year":"2006","journal-title":"Proc IEEE Symp Security Privacy"},{"key":"ref103","doi-asserted-by":"publisher","DOI":"10.1109\/ICNP.2009.5339690"},{"key":"ref102","doi-asserted-by":"publisher","DOI":"10.1145\/1544012.1544021"},{"key":"ref111","article-title":"Network verification in the light of program verification","author":"lopes","year":"2013"},{"key":"ref112","article-title":"Automated analysis and debugging of network connectivity policies","author":"lopes","year":"2013"},{"key":"ref110","doi-asserted-by":"publisher","DOI":"10.1145\/285243.285283"},{"key":"ref98","doi-asserted-by":"crossref","first-page":"811","DOI":"10.1007\/978-3-662-49674-9_51","article-title":"Some complexity results for stateful network verification","author":"velner","year":"2016","journal-title":"Proc Int Conf Tools Algorithms Construct Anal Syst"},{"key":"ref99","doi-asserted-by":"publisher","DOI":"10.1109\/TNET.2013.2253121"},{"key":"ref96","first-page":"217","article-title":"Efficient network reachability analysis using a succinct control plane representation","author":"fayaz","year":"2016","journal-title":"Proc of USENIX Symp on Operating Systems Design and Implementation (OSDI)"},{"key":"ref97","doi-asserted-by":"publisher","DOI":"10.1145\/2829988.2790012"},{"key":"ref10","first-page":"155","article-title":"Model checking large network protocol implementations","author":"musuvathi","year":"2004","journal-title":"Proc 1st Symp Networked Syst Design Implem (NSDI)"},{"key":"ref11","author":"muuss","year":"2014","journal-title":"[Online]"},{"key":"ref12","author":"jacobson","year":"2015","journal-title":"[Online]"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0183-4"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1109\/SURV.2014.012214.00180"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2014.2371999"},{"key":"ref118","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1145\/1030194.1015472","article-title":"Routing design in operational networks","volume":"34","author":"maltz","year":"2004","journal-title":"ACM SIGCOMM Comput Commun Rev"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/COMST.2014.2326417"},{"key":"ref82","doi-asserted-by":"publisher","DOI":"10.1145\/1995376.1995394"},{"key":"ref117","doi-asserted-by":"publisher","DOI":"10.1145\/1402946.1402964"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1016\/j.comnet.2015.02.014"},{"key":"ref81","doi-asserted-by":"publisher","DOI":"10.1145\/1536616.1536637"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1109\/TR.2015.2421391"},{"key":"ref84","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1145\/1177352.1177354","article-title":"Propositional satisfiability and constraint programming: A comparative survey","volume":"38","author":"hamadi","year":"2006","journal-title":"ACM Comput Surveys"},{"key":"ref119","first-page":"237","article-title":"Using service grammar to diagnose BGP configuration errors","author":"qie","year":"2003","journal-title":"Proc 17th Conf Syst Admin (LISA)"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/COMST.2014.2345792"},{"key":"ref83","first-page":"825","article-title":"Satisfiability modulo theories","author":"barrett","year":"2009","journal-title":"Handbook of Satisfiability"},{"key":"ref114","first-page":"699","article-title":"Verifying reachability in networks with mutable datapaths","author":"panda","year":"2017","journal-title":"Proc USENIX Symp Netw Syst Design Implem (NSDI)"},{"key":"ref113","doi-asserted-by":"publisher","DOI":"10.1145\/1592568.1592595"},{"key":"ref116","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/978-3-319-49052-6_4","article-title":"ddNF: An efficient data structure for header spaces","author":"bj\u00f8rner","year":"2016","journal-title":"Hardware and Software Verification and Testing"},{"key":"ref80","first-page":"547","article-title":"Inherently safe backup routing with BGP","volume":"1","author":"gao","year":"2001","journal-title":"Proc IEEE InfoCom"},{"key":"ref115","doi-asserted-by":"publisher","DOI":"10.1145\/2535828.2535835"},{"key":"ref120","doi-asserted-by":"publisher","DOI":"10.1016\/S1389-1286(99)00108-5"},{"key":"ref89","doi-asserted-by":"publisher","DOI":"10.1145\/3098822.3098834"},{"key":"ref121","doi-asserted-by":"publisher","DOI":"10.1109\/90.993304"},{"key":"ref122","first-page":"43","article-title":"Detecting BGP configuration faults with static analysis (awarded best paper)","author":"feamster","year":"2005","journal-title":"Proc 2nd Symposium Networked Syst Design and Implementation (NSDI)"},{"key":"ref123","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80473-0"},{"key":"ref85","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-4129-7"},{"key":"ref86","year":"2007","journal-title":"SAT-Based Verification Framework"},{"key":"ref87","doi-asserted-by":"publisher","DOI":"10.1016\/S1574-6526(07)03002-7"},{"key":"ref88","doi-asserted-by":"publisher","DOI":"10.1145\/1831708.1831710"}],"container-title":["IEEE Communications Surveys & Tutorials"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/9739\/8649699\/08453007.pdf?arnumber=8453007","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,6]],"date-time":"2025-07-06T19:04:26Z","timestamp":1751828666000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8453007\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"references-count":183,"journal-issue":{"issue":"1"},"URL":"https:\/\/doi.org\/10.1109\/comst.2018.2868050","relation":{},"ISSN":["1553-877X","2373-745X"],"issn-type":[{"value":"1553-877X","type":"electronic"},{"value":"2373-745X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]}}}