{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,20]],"date-time":"2026-09-20T10:46:30Z","timestamp":1789901190772,"version":"4.0.1"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319955810","type":"print"},{"value":"9783319955827","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-95582-7_33","type":"book-chapter","created":{"date-parts":[[2018,7,11]],"date-time":"2018-07-11T14:31:17Z","timestamp":1531319477000},"page":"550-567","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["SDN-Actors: Modeling and Verification of SDN Programs"],"prefix":"10.1007","author":[{"given":"Elvira","family":"Albert","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Miguel","family":"G\u00f3mez-Zamalloa","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Albert","family":"Rubio","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matteo","family":"Sammartino","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alexandra","family":"Silva","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2018,7,12]]},"reference":[{"key":"33_CR1","unstructured":"The ABS tool suite. http:\/\/abs-models.org"},{"key":"33_CR2","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/1086.001.0001","volume-title":"Actors: A Model of Concurrent Computation in Distributed Systems","author":"G Agha","year":"1986","unstructured":"Agha, G.: Actors: A Model of Concurrent Computation in Distributed Systems. MIT Press, Cambridge (1986)"},{"key":"33_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"526","DOI":"10.1007\/978-3-319-63387-9_26","volume-title":"Computer Aided Verification","author":"E Albert","year":"2017","unstructured":"Albert, E., Arenas, P., de la Banda, M.G., G\u00f3mez-Zamalloa, M., Stuckey, P.J.: Context-sensitive dynamic partial order reduction. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 526\u2013543. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_26"},{"key":"33_CR4","doi-asserted-by":"crossref","unstructured":"Albert, E., G\u00f3mez-Zamalloa, M., Isabel, M.: SYCO: a systematic testing tool for concurrent objects. In: CC, pp. 269\u2013270 (2016)","DOI":"10.1145\/2892208.2892236"},{"key":"33_CR5","unstructured":"Albert, E., G\u00f3mez-Zamalloa, M., Rubio, A., Sammartino, M., Silva, A.: SDN-Actors: Modeling and Verification of SDN Programs. Technical report (2018). http:\/\/costa.ls.fi.upm.es\/papers\/costa\/AlbertGRSS18TR.pdf"},{"issue":"6","key":"33_CR6","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1145\/2666356.2594317","volume":"49","author":"Thomas Ball","year":"2014","unstructured":"Ball, T., Bj\u00f8rner, N., Gember, A., Itzhaky, S., Karbyshev, A., Sagiv, M., Schapira, M., Valadarsky, A.: VeriCon: towards verifying controller programs in software-defined networks. In: PLDI, pp. 282\u2013293 (2014)","journal-title":"ACM SIGPLAN Notices"},{"issue":"1","key":"33_CR7","doi-asserted-by":"publisher","first-page":"651","DOI":"10.1145\/2775051.2677002","volume":"50","author":"Ahmed Bouajjani","year":"2015","unstructured":"Bouajjani, A., Emmi, M., Enea, C., Hamza, J.: Tractable refinement checking for concurrent objects. In: POPL, pp. 651\u2013662 (2015)","journal-title":"ACM SIGPLAN Notices"},{"key":"33_CR8","unstructured":"Canini, M., Venzano, D., Peres\u00edni, P., Kostic, D., Rexford, J.: A NICE way to test OpenFlow applications. In: NSDI, pp. 127\u2013140 (2012)"},{"key":"33_CR9","doi-asserted-by":"crossref","unstructured":"Christakis, M., Gotovos, A., Sagonas, K.F.: Systematic testing for detecting concurrency errors in Erlang programs. In: ICST, pp. 154\u2013163 (2013)","DOI":"10.1109\/ICST.2013.50"},{"key":"33_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1007\/978-3-540-71316-6_22","volume-title":"Programming Languages and Systems","author":"FS Boer de","year":"2007","unstructured":"de Boer, F.S., Clarke, D., Johnsen, E.B.: A complete guide to the future. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 316\u2013330. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71316-6_22"},{"key":"33_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/978-3-642-37635-1_9","volume-title":"Recent Trends in Algebraic Development Techniques","author":"J Eckhardt","year":"2013","unstructured":"Eckhardt, J., M\u00fchlbauer, T., Meseguer, J., Wirsing, M.: Statistical model checking for composite actor systems. In: Mart\u00ed-Oliet, N., Palomino, M. (eds.) WADT 2012. LNCS, vol. 7841, pp. 143\u2013160. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37635-1_9"},{"issue":"6","key":"33_CR12","doi-asserted-by":"publisher","first-page":"402","DOI":"10.1145\/2980983.2908124","volume":"51","author":"Ahmed El-Hassany","year":"2016","unstructured":"El-Hassany, A., Miserez, J., Bielik, P., Vanbever, L., Vechev, M.T.: SDNRacer: concurrency analysis for software-defined networks. In: POPL, pp. 402\u2013415 (2016)","journal-title":"ACM SIGPLAN Notices"},{"issue":"1","key":"33_CR13","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1145\/1047659.1040315","volume":"40","author":"Cormac Flanagan","year":"2005","unstructured":"Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: POPL, pp. 110\u2013121 (2005)","journal-title":"ACM SIGPLAN Notices"},{"key":"33_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-642-25271-6_8","volume-title":"Formal Methods for Components and Objects","author":"EB Johnsen","year":"2011","unstructured":"Johnsen, E.B., H\u00e4hnle, R., Sch\u00e4fer, J., Schlatte, R., Steffen, M.: ABS: a core language for abstract behavioral specification. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 142\u2013164. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-25271-6_8"},{"key":"33_CR15","unstructured":"Kazemian, P., Varghese, G., McKeown, N.: Header space analysis: static checking for networks. In: NSDI, pp. 113\u2013126 (2012)"},{"key":"33_CR16","doi-asserted-by":"crossref","unstructured":"Lauterburg, S., Karmani, R.K., Marinov, D., Agha, G.: Basset: a tool for systematic testing of actor programs. In: SIGSOFT FSE, pp. 363\u2013364 (2010)","DOI":"10.1145\/1882291.1882349"},{"issue":"1","key":"33_CR17","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/2914770.2837635","volume":"51","author":"Hongjin Liang","year":"2016","unstructured":"Liang, H., Feng, X.: A program logic for concurrent objects under fair scheduling. In: POPL, pp. 385\u2013399 (2016)","journal-title":"ACM SIGPLAN Notices"},{"key":"33_CR18","doi-asserted-by":"crossref","unstructured":"Majumdar, R., Tetali, S.D., Wang, Z.: Kuai: a model checker for software-defined networks. In: FMCAD, pp. 163\u2013170 (2014)","DOI":"10.1109\/FMCAD.2014.6987609"},{"key":"33_CR19","unstructured":"Openflow switch specification, October 2013. Version 1.4.0. http:\/\/www.opennetworking.org\/software-defined-standards\/specifications"},{"key":"33_CR20","series-title":"IFIP Advances in Information and Communication Technology","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-319-58469-0_2","volume-title":"ICT Systems Security and Privacy Protection","author":"TA Pascoal","year":"2017","unstructured":"Pascoal, T.A., Dantas, Y.G., Fonseca, I.E., Nigam, V.: Slow TCAM exhaustion DDoS attack. In: De Capitani di Vimercati, S., Martinelli, F. (eds.) SEC 2017. IAICT, vol. 502, pp. 17\u201331. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-58469-0_2"},{"key":"33_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/11693017_25","volume-title":"Fundamental Approaches to Software Engineering","author":"K Sen","year":"2006","unstructured":"Sen, K., Agha, G.: Automated systematic testing of open distributed programs. In: Baresi, L., Heckel, R. (eds.) FASE 2006. LNCS, vol. 3922, pp. 339\u2013356. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11693017_25"},{"key":"33_CR22","doi-asserted-by":"crossref","unstructured":"Sethi, D., Narayana, S., Malik, S.: Abstractions for model checking SDN controllers. In: FMCAD, pp. 145\u2013148 (2013)","DOI":"10.1109\/FMCAD.2013.6679403"},{"key":"33_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/978-3-642-30793-5_14","volume-title":"Formal Techniques for Distributed Systems","author":"S Tasharofi","year":"2012","unstructured":"Tasharofi, S., et al.: TransDPOR: a novel dynamic partial-order reduction technique for testing actor programs. In: Giese, H., Rosu, G. (eds.) FMOODS\/FORTE -2012. LNCS, vol. 7273, pp. 219\u2013234. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-30793-5_14"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-95582-7_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,5]],"date-time":"2020-11-05T16:06:41Z","timestamp":1604592401000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-95582-7_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319955810","9783319955827"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-95582-7_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}