{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T06:49:11Z","timestamp":1726037351845},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030255428"},{"type":"electronic","value":"9783030255435"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-25543-5_18","type":"book-chapter","created":{"date-parts":[[2019,7,12]],"date-time":"2019-07-12T12:03:09Z","timestamp":1562932989000},"page":"305-323","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Efficient Verification of Network Fault Tolerance via Counterexample-Guided Refinement"],"prefix":"10.1007","author":[{"given":"Nick","family":"Giannarakis","sequence":"first","affiliation":[]},{"given":"Ryan","family":"Beckett","sequence":"additional","affiliation":[]},{"given":"Ratul","family":"Mahajan","sequence":"additional","affiliation":[]},{"given":"David","family":"Walker","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,7,12]]},"reference":[{"key":"18_CR1","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 203\u2013213 (2001)","DOI":"10.1145\/381694.378846"},{"key":"18_CR2","doi-asserted-by":"crossref","unstructured":"Beckett, R., Gupta, A., Mahajan, R., Walker, D.: A general approach to network configuration verification. In: SIGCOMM, August 2017","DOI":"10.1145\/3098822.3098834"},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"Beckett, R., Gupta, A., Mahajan, R., Walker, D.: Control plane compression. In: Proceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication, pp. 476\u2013489. ACM (2018)","DOI":"10.1145\/3230543.3230583"},{"key":"18_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/3-540-56922-7_37","volume-title":"Computer Aided Verification","author":"EM Clarke","year":"1993","unstructured":"Clarke, E.M., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 450\u2013462. Springer, Heidelberg (1993). \n                      https:\/\/doi.org\/10.1007\/3-540-56922-7_37"},{"key":"18_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154\u2013169. Springer, Heidelberg (2000). \n                      https:\/\/doi.org\/10.1007\/10722167_15"},{"issue":"5","key":"18_CR6","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"EM Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512\u20131542 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"Daggitt, M.L., Gurney, A.J.T., Griffin, T.G.: Asynchronous convergence of policy-rich distributed bellman-ford routing protocols. In: SIGCOMM, pp. 103\u2013116 (2018)","DOI":"10.1145\/3230543.3230561"},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"Daggitt, M.L., Gurney, A.J., Griffin, T.G.: Asynchronous convergence of policy-rich distributed Bellman-Ford routing protocols. In: Proceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication, pp. 103\u2013116. ACM (2018)","DOI":"10.1145\/3230543.3230561"},{"key":"18_CR9","unstructured":"Das, S., Dill, D.L.: Successive approximation of abstract transition relations. In: Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, LICS 2001, p. 51 (2001)"},{"key":"18_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). \n                      https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"issue":"2","key":"18_CR11","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1109\/TNET.2007.892876","volume":"15","author":"N Feamster","year":"2007","unstructured":"Feamster, N., Rexford, J.: Network-wide prediction of BGP routes. IEEE\/ACM Trans. Netw. 15(2), 253\u2013266 (2007)","journal-title":"IEEE\/ACM Trans. Netw."},{"key":"18_CR12","unstructured":"Fogel, A., et al.: A general approach to network configuration analysis. In: NSDI (2015)"},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"Gember-Jacobson, A., Viswanathan, R., Akella, A., Mahajan, R.: Fast control plane analysis using an abstract representation. In: SIGCOMM (2016)","DOI":"10.1145\/2934872.2934876"},{"key":"18_CR14","doi-asserted-by":"crossref","unstructured":"Gill, P., Jain, N., Nagappan, N.: Understanding network failures in data centers: measurement, analysis, and implications. In: SIGCOMM (2011)","DOI":"10.1145\/2018436.2018477"},{"key":"18_CR15","unstructured":"Godfrey, J.: The summer of network misconfigurations (2016). \n                      https:\/\/blog.algosec.com\/2016\/08\/business-outages-caused-misconfigurations-headline-news-summer.html"},{"issue":"2","key":"18_CR16","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1109\/90.993304","volume":"10","author":"TG Griffin","year":"2002","unstructured":"Griffin, T.G., Shepherd, F.B., Wilfong, G.: The stable paths problem and interdomain routing. IEEE\/ACM Trans. Netw. 10(2), 232\u2013243 (2002)","journal-title":"IEEE\/ACM Trans. Netw."},{"issue":"4","key":"18_CR17","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/s100090050040","volume":"2","author":"Y Kesten","year":"2000","unstructured":"Kesten, Y., Pnueli, A.: Control and data abstraction: the cornerstones of practical formal verification. Softw. Tools Technol. Transf. 2(4), 328\u2013342 (2000)","journal-title":"Softw. Tools Technol. Transf."},{"key":"18_CR18","doi-asserted-by":"crossref","unstructured":"Lapukhov, P., Premji, A., Mitchell, J.: Use of BGP for routing in large-scale data centers. Internet draft (2015)","DOI":"10.17487\/RFC7938"},{"key":"18_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/978-3-030-11245-5_18","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"NP Lopes","year":"2019","unstructured":"Lopes, N.P., Rybalchenko, A.: Fast BGP simulation of large datacenters. In: Enea, C., Piskac, R. (eds.) VMCAI 2019. LNCS, vol. 11388, pp. 386\u2013408. Springer, Cham (2019). \n                      https:\/\/doi.org\/10.1007\/978-3-030-11245-5_18"},{"key":"18_CR20","unstructured":"Lougheed, K.: A border gateway protocol (BGP). RFC 1163, RFC Editor (1989). \n                      http:\/\/www.rfc-editor.org\/rfc\/rfc1163.txt"},{"key":"18_CR21","doi-asserted-by":"crossref","unstructured":"Mahajan, R., Wetherall, D., Anderson, T.: Understanding BGP misconfiguration. In: SIGCOMM (2002)","DOI":"10.1145\/633026.633027"},{"key":"18_CR22","doi-asserted-by":"crossref","unstructured":"Plotkin, G.D., Bj\u00f8rner, N., Lopes, N.P., Rybalchenko, A., Varghese, G.: Scaling network verification using symmetry and surgery. In: POPL (2016)","DOI":"10.1145\/2837614.2837657"},{"issue":"6","key":"18_CR23","first-page":"12","volume":"19","author":"B Quoitin","year":"2005","unstructured":"Quoitin, B., Uhlig, S.: Modeling the routing of an autonomous system with C-BGP. Netw. Mag. Glob. Internetworking 19(6), 12\u201319 (2005)","journal-title":"Netw. Mag. Glob. Internetworking"},{"issue":"5","key":"18_CR24","doi-asserted-by":"publisher","first-page":"1160","DOI":"10.1109\/TNET.2005.857111","volume":"13","author":"JAL Sobrinho","year":"2005","unstructured":"Sobrinho, J.A.L.: An algebraic theory of dynamic network routing. IEEE\/ACM Trans. Netw. 13(5), 1160\u20131173 (2005)","journal-title":"IEEE\/ACM Trans. Netw."},{"key":"18_CR25","unstructured":"Weitz, K., Woos, D., Torlak, E., Ernst, M.D., Krishnamurthy, A., Tatlock, Z.: Formal semantics and automated verification for the border gateway protocol. In: NetPL (2016)"}],"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-25543-5_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,12]],"date-time":"2019-07-12T12:08:21Z","timestamp":1562933301000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-25543-5_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030255428","9783030255435"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-25543-5_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"12 July 2019","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":"New York City, NY","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":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 July 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 July 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav0","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2019\/","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","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"258","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":"67","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":"0","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":"26% - 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":"3","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":"9","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":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}