{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T23:09:29Z","timestamp":1743030569549,"version":"3.40.3"},"publisher-location":"Cham","reference-count":51,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030532901"},{"type":"electronic","value":"9783030532918"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,7,14]],"date-time":"2020-07-14T00:00:00Z","timestamp":1594684800000},"content-version":"vor","delay-in-days":195,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-53291-8_8","type":"book-chapter","created":{"date-parts":[[2020,7,15]],"date-time":"2020-07-15T20:03:35Z","timestamp":1594843415000},"page":"126-148","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Towards Model Checking Real-World Software-Defined Networks"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3173-8636","authenticated-orcid":false,"given":"Vasileios","family":"Klimis","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1298-7143","authenticated-orcid":false,"given":"George","family":"Parisis","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5807-856X","authenticated-orcid":false,"given":"Bernhard","family":"Reus","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,7,14]]},"reference":[{"key":"8_CR1","unstructured":"Al-Fares, M., Radhakrishnan, S., Raghavan, B.: Hedera: dynamic flow scheduling for data center networks. In: NSDI (2010)"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Al-Shaer, E., Al-Haj, S.: FlowChecker: configuration analysis and verification of federated OpenFlow infrastructures. In: SafeConfig (2010)","DOI":"10.1145\/1866898.1866905"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"550","DOI":"10.1007\/978-3-319-95582-7_33","volume-title":"Formal Methods","author":"E Albert","year":"2018","unstructured":"Albert, E., G\u00f3mez-Zamalloa, M., Rubio, A., Sammartino, M., Silva, A.: SDN-Actors: modeling and verification of SDN programs. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds.) FM 2018. LNCS, vol. 10951, pp. 550\u2013567. Springer, Cham (2018)"},{"key":"8_CR4","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press, Cambridge (2008)"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"Ball, T., Bj\u00f8rner, N., Gember, A., et al.: VeriCon: towards verifying controller programs in software-defined networks. In: PLDI (2014)","DOI":"10.1145\/2594291.2594317"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Behrmann, G., David, A., Larsen, K.G., et al.: Developing UPPAAL over 15 years. In: Practice and Experience, Software (2011)","DOI":"10.1002\/spe.1006"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Braga, R., Mota, E., Passito, A.: Lightweight DDoS flooding attack detection using NOX\/OpenFlow. In: LCN (2010)","DOI":"10.1109\/LCN.2010.5735752"},{"key":"8_CR8","unstructured":"Canini, M., Venzano, D., Pere\u0161\u00edni, P., et al.: A NICE way to test OpenFlow applications. In: NSDI (2012)"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2002","unstructured":"Cimatti, A., et al.: NuSMV 2: an OpenSource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359\u2013364. Springer, Heidelberg (2002)"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Curtis, A.R., Mogul, J.C., Tourrilhes, J., et al.: DevoFlow: scaling flow management for high-performance networks. In: SIGCOMM (2011)","DOI":"10.1145\/2018436.2018466"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Dobrescu, M., Argyraki, K.: Software dataplane verification. In: Communications of the ACM (2015)","DOI":"10.1145\/2823400"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/978-3-319-63390-9_14","volume-title":"Computer Aided Verification","author":"A El-Hassany","year":"2017","unstructured":"El-Hassany, A., Tsankov, P., Vanbever, L., Vechev, M.: Network-wide configuration synthesis. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 261\u2013281. Springer, Cham (2017)"},{"key":"8_CR13","unstructured":"Fayaz, S.K., Sharma, T., Fogel, A., et al.: Efficient network reachability analysis using a succinct control plane representation. In: OSDI (2016)"},{"key":"8_CR14","unstructured":"Fayaz, S.K., Yu, T., Tobioka, Y., et al.: BUZZ: testing context-dependent policies in stateful networks. In: NSDI (2016)"},{"key":"8_CR15","unstructured":"Feamster, N., Rexford, J., Shenker, S., et al.: SDX: A Software-defined Internet Exchange. Open Networking Summit (2013)"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"Feamster, N., Rexford, J., Zegura, E.: The road to SDN. SIGCOMM Comput. Commun. Rev. (2014)","DOI":"10.1145\/2602204.2602219"},{"key":"8_CR17","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"MJ Fischer","year":"1979","unstructured":"Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18, 194\u2013211 (1979)","journal-title":"J. Comput. Syst. Sci."},{"key":"8_CR18","unstructured":"Fogel, A., Fung, S., Angeles, L., et al.: A general approach to network configuration analysis. In: NSDI (2015)"},{"key":"8_CR19","unstructured":"Handigol, N., Seetharaman, S., Flajslik, M., et al.: Plug-n-Serve: load-balancing web traffic using OpenFlow. In: SIGCOMM (2009)"},{"key":"8_CR20","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/s100090050043","volume":"2","author":"K Havelund","year":"2000","unstructured":"Havelund, K., Pressburger, T.: Model checking JAVA programs using JAVA PathFinder. STTT 2, 366\u2013381 (2000)","journal-title":"STTT"},{"key":"8_CR21","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23, 279\u2013295 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J., Peled, D.: An improvement in formal verification. In: Hogrefe D., Leue S. (eds) Formal Description Techniques VII. IAICT, pp. 197\u2013211. Springer, Boston, MA (1995)","DOI":"10.1007\/978-0-387-34878-0_13"},{"key":"8_CR23","unstructured":"Horn, A., Kheradmand, A., Prasad, M.R.: Delta-net: real-time network verification using atoms. In: NSDI (2017)"},{"key":"8_CR24","unstructured":"Hu, H., Ahn, G.J., Han, W., et al.: Towards a reliable SDN firewall. In: ONS (2014)"},{"key":"8_CR25","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1145\/505145.505149","volume":"11","author":"D Jackson","year":"2002","unstructured":"Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol. 11, 256\u2013290 (2002)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"8_CR26","doi-asserted-by":"crossref","unstructured":"Jafarian, J.H., Al-Shaer, E., Duan, Q.: OpenFlow random host mutation: transparent moving target defense using software defined networking. In: HotSDN (2012)","DOI":"10.1145\/2342441.2342467"},{"key":"8_CR27","doi-asserted-by":"crossref","unstructured":"Jain, S., Zhu, M., Zolla, J., et al.: B4: experience with a globally-deployed software defined WAN. In: SIGCOMM (2013)","DOI":"10.1145\/2486001.2486019"},{"key":"8_CR28","unstructured":"Jia, Y.: NetSMC: a symbolic model checker for stateful network verification. In: NSDI (2020)"},{"key":"8_CR29","unstructured":"Kazemian, P., Chang, M., Zeng, H., et al.: Real time network policy checking using header space analysis. In: NSDI (2013)"},{"key":"8_CR30","unstructured":"Kazemian, P., Varghese, G., McKeown, N.: Header space analysis: static checking for networks. In: NSDI (2012)"},{"key":"8_CR31","doi-asserted-by":"crossref","unstructured":"Khurshid, A., Zou, X., Zhou, W., et al.: VeriFlow: verifying network-wide invariants in real time. In: NSDI (2013)","DOI":"10.1145\/2342441.2342452"},{"key":"8_CR32","doi-asserted-by":"crossref","unstructured":"Klimis, V., Parisis, G., Reus, B.: Towards model checking real-world software-defined networks (version with appendix). preprint arXiv:2004.11988 (2020)","DOI":"10.1007\/978-3-030-53291-8_8"},{"key":"8_CR33","doi-asserted-by":"publisher","first-page":"940","DOI":"10.1109\/COMST.2018.2868050","volume":"21","author":"Y Li","year":"2019","unstructured":"Li, Y., Yin, X., Wang, Z., et al.: A survey on network verification and testing with formal methods: approaches and challenges. IEEE Surv. Tutorials 21, 940\u2013969 (2019)","journal-title":"IEEE Surv. Tutorials"},{"key":"8_CR34","doi-asserted-by":"crossref","unstructured":"Mai, H., Khurshid, A., Agarwal, R., et al.: Debugging the data plane with anteater. In: SIGCOMM (2011)","DOI":"10.1145\/2018436.2018470"},{"key":"8_CR35","doi-asserted-by":"crossref","unstructured":"Majumdar, R., Deep Tetali, S., Wang, Z.: Kuai: a model checker for software-defined networks. In: FMCAD (2014)","DOI":"10.1109\/FMCAD.2014.6987609"},{"key":"8_CR36","doi-asserted-by":"crossref","unstructured":"McClurg, J., Hojjat, H., \u010cern\u00fd, P., et al.: Efficient synthesis of network updates. In: PLDI (2015)","DOI":"10.1145\/2737924.2737980"},{"key":"8_CR37","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1145\/1355734.1355746","volume":"38","author":"N McKeown","year":"2008","unstructured":"McKeown, N., Anderson, T., Balakrishnan, H., et al.: OpenFlow: enabling innovation in campus networks. SIGCOMM Comput. Commun. Rev. 38, 69\u201374 (2008)","journal-title":"SIGCOMM Comput. Commun. Rev."},{"key":"8_CR38","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1145\/2534169.2486026","volume":"43","author":"P Patel","year":"2013","unstructured":"Patel, P., Bansal, D., Yuan, L., et al.: Ananta: cloud scale load balancing. SIGCOMM 43, 207\u2013218 (2013)","journal-title":"SIGCOMM"},{"key":"8_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/3-540-56922-7_34","volume-title":"Computer Aided Verification","author":"D Peled","year":"1993","unstructured":"Peled, D.: All from one, one for all: on model checking using representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 409\u2013423. Springer, Heidelberg (1993)"},{"key":"8_CR40","doi-asserted-by":"crossref","unstructured":"Plotkin, G.D., Bj\u00f8rner, N., Lopes, N.P., et al.: Scaling network verification using symmetry and surgery. In: POPL (2016)","DOI":"10.1145\/2837614.2837657"},{"key":"8_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/3-540-45657-0_9","volume-title":"Computer Aided Verification","author":"A Pnueli","year":"2002","unstructured":"Pnueli, A., Xu, J., Zuck, L.: Liveness with (0,1, $$\\infty $$)- counter abstraction. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 107\u2013122. Springer, Heidelberg (2002)"},{"key":"8_CR42","doi-asserted-by":"crossref","unstructured":"Pratt, V.R.: Semantical considerations on Floyd-Hoare logic. In: FOCS (1976)","DOI":"10.1109\/SFCS.1976.27"},{"key":"8_CR43","doi-asserted-by":"crossref","unstructured":"Sethi, D., Narayana, S., Malik, S.: Abstractions for model checking SDN controllers. In: FMCAD (2013)","DOI":"10.1109\/FMCAD.2013.6679403"},{"key":"8_CR44","unstructured":"Shenker, S., Casado, M., Koponen, T., et al.: The future of networking, and the past of protocols. In: ONS (2011). https:\/\/tinyurl.com\/yxnuxobt"},{"key":"8_CR45","doi-asserted-by":"crossref","unstructured":"Son, S., Shin, S., Yegneswaran, V., et al.: Model checking invariant security properties in OpenFlow. In: IEEE (2013)","DOI":"10.1109\/ICC.2013.6654813"},{"key":"8_CR46","doi-asserted-by":"crossref","unstructured":"Stoenescu, R., Popovici, M., Negreanu, L., et al.: SymNet: scalable symbolic execution for modern networks. In: SIGCOMM (2016)","DOI":"10.1145\/2934872.2934881"},{"key":"8_CR47","unstructured":"Varghese, G.: Vision for network design automation and network verification. In: NetPL (Talk) (2018). https:\/\/tinyurl.com\/y2cnhvhf"},{"key":"8_CR48","doi-asserted-by":"publisher","first-page":"887","DOI":"10.1109\/TNET.2015.2398197","volume":"24","author":"H Yang","year":"2016","unstructured":"Yang, H., Lam, S.S.: Real-time verification of network properties using atomic predicates. IEEE\/ACM Trans. Network. 24, 887\u2013900 (2016)","journal-title":"IEEE\/ACM Trans. Network."},{"key":"8_CR49","unstructured":"Zeng, H., Kazemian, P., Varghese, G., et al.: A survey on network troubleshooting. Technical report TR12-HPNG-061012, Stanford University (2012)"},{"key":"8_CR50","unstructured":"Zeng, H., Zhang, S., Ye, F., et al.: Libra: divide and conquer to verify forwarding tables in huge networks. In: NSDI (2014)"},{"key":"8_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"496","DOI":"10.1007\/978-3-319-02444-8_43","volume-title":"Automated Technology for Verification and Analysis","author":"S Zhang","year":"2013","unstructured":"Zhang, S., Malik, S.: SAT based verification of network data planes. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 496\u2013505. Springer, Cham (2013)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-53291-8_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,25]],"date-time":"2021-03-25T05:59:37Z","timestamp":1616651977000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-53291-8_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030532901","9783030532918"],"references-count":51,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-53291-8_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"14 July 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Los Angeles, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"32","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair.org","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"240","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"43","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"22","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"18% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference was held virtually due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}