{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T15:37:57Z","timestamp":1759333077276,"version":"3.40.3"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319633893"},{"type":"electronic","value":"9783319633909"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-63390-9_16","type":"book-chapter","created":{"date-parts":[[2017,7,12]],"date-time":"2017-07-12T08:53:50Z","timestamp":1499849630000},"page":"301-321","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Synchronization Synthesis for Network Programs"],"prefix":"10.1007","author":[{"given":"Jedidiah","family":"McClurg","sequence":"first","affiliation":[]},{"given":"Hossein","family":"Hojjat","sequence":"additional","affiliation":[]},{"given":"Pavol","family":"\u010cern\u00fd","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,7,13]]},"reference":[{"key":"16_CR1","unstructured":"Anderson, C.J., Foster, N., Guha, A., Jeannin, J.-B., Kozen, D., Schlesinger, C., Walker, D.: NetKAT: semantic foundations for networks. In: POPL (2014)"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Arashloo, M.T., Koral, Y., Greenberg, M., Rexford, J., Walker, D.: SNAP: stateful network-wide abstractions for packet processing. In: SIGCOMM (2016)","DOI":"10.1145\/2934872.2934892"},{"issue":"1\u20132","key":"16_CR3","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1016\/S0304-3975(96)00219-8","volume":"186","author":"E Badouel","year":"1997","unstructured":"Badouel, E., Bernardinello, L., Darondeau, P.: The synthesis problem for elementary net systems is NP-complete. Theor. Comput. Sci. 186(1\u20132), 107\u2013134 (1997)","journal-title":"Theor. Comput. Sci."},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Basile, F., Chiacchio, P., Coppola, J.: Model repair of time petri nets with temporal anomalies. In: IFAC (2015)","DOI":"10.1016\/j.ifacol.2015.06.477"},{"issue":"4","key":"16_CR5","first-page":"437","volume":"88","author":"R Bergenthum","year":"2008","unstructured":"Bergenthum, R., Desel, J., Lorenz, R., Mauser, S.: Synthesis of petri nets from finite partial languages. Fundam. Inform. 88(4), 437\u2013468 (2008)","journal-title":"Fundam. Inform."},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"Bianchi, G., Bonola, M., Capone, A., Cascone, C.: Open-State: programming platform-independent stateful openflow applications inside the switch. In: ACM SIGCOMM CCR (2014)","DOI":"10.1145\/2602204.2602211"},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"Bloem, R., Hofferek, G., K\u00f6nighofer, B., K\u00f6nighofer, R., Ausserlechner, S., Spork, R.: Synthesis of synchronization using uninterpreted functions. In: FMCAD. IEEE (2014)","DOI":"10.1109\/FMCAD.2014.6987593"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"Bosshart, P., Daly, D., Gibb, G., Izzard, M., McKeown, N., Rexford, J., Schlesinger, C., Talayco, D., Vahdat, A., Varghese, G., et al.: P4: programming protocol-independent packet processors. In: ACM SIG- COMM CCR (2014)","DOI":"10.1145\/2656877.2656890"},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"Canini, M., Kuznetsov, P., Levin, D., Schmid, S.: Software transactional networking: concurrent and consistent policy composition. In: HotSDN (2013)","DOI":"10.1145\/2491185.2491200"},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"951","DOI":"10.1007\/978-3-642-39799-8_68","volume-title":"Computer Aided Verification","author":"P \u010cern\u00fd","year":"2013","unstructured":"\u010cern\u00fd, P., Henzinger, T.A., Radhakrishna, A., Ryzhyk, L., Tarrach, T.: Efficient synthesis for concurrency by semantics-preserving transformations. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 951\u2013967. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-39799-8_68"},{"key":"16_CR11","unstructured":"Cortadella, J., Kishinevsky, M., Lavagno, L., Yakovlev, A.: Synthesizing petri nets from state-based models. In: ICCAD (1995)"},{"issue":"4","key":"16_CR12","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/s002360050046","volume":"33","author":"J Desel","year":"1996","unstructured":"Desel, J., Reisig, W.: The synthesis problem of petri nets. Acta Inf. 33(4), 297\u2013315 (1996)","journal-title":"Acta Inf."},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"Dixit, A.A., Hao, F., Mukherjee, S., Lakshman, T.V., Kompella, R.: ElastiCon: an elastic distributed SDN controller. In: ANCS (2014)","DOI":"10.1145\/2658260.2658261"},{"key":"16_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-319-19488-2_2","volume-title":"Application and Theory of Petri Nets and Concurrency","author":"M Dumas","year":"2015","unstructured":"Dumas, M., Garc\u00eda-Ba\u00f1uelos, L.: Process mining reloaded: event structures as a unified representation of process models and event logs. In: Devillers, R., Valmari, A. (eds.) PETRI NETS 2015. LNCS, vol. 9115, pp. 33\u201348. Springer, Cham (2015). doi:10.1007\/978-3-319-19488-2_2"},{"issue":"4","key":"16_CR15","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/BF00264612","volume":"27","author":"A Ehrenfeucht","year":"1990","unstructured":"Ehrenfeucht, A., Rozenberg, G.: Partial (Set) 2-structures. Part II: state spaces of concurrent systems. Acta Inf. 27(4), 343\u2013368 (1990)","journal-title":"Acta Inf."},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"El-Hassany, A., Miserez, J., Bielik, P., Vanbever, L., Vechev, M.T.: SDNRacer: concurrency analysis for software-defined networks. In: PLDI (2016)","DOI":"10.1145\/2908080.2908124"},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Jha, S., Tiwari, A., Venkatesan, R.: Synthesis of loop-free programs. In: PLDI (2011)","DOI":"10.1145\/1993498.1993506"},{"key":"16_CR18","doi-asserted-by":"crossref","unstructured":"Hojjat, H., Ruemmer, P., McClurg, J., Cerny, P., Foster, N.: Optimizing horn solvers for network repair. In: FMCAD (2016)","DOI":"10.1109\/FMCAD.2016.7886663"},{"key":"16_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/BFb0019974","volume-title":"Advances in Petri Nets 1991","author":"RP Hopkins","year":"1991","unstructured":"Hopkins, R.P.: Distributable nets. In: Rozenberg, G. (ed.) ICATPN 1990. LNCS, vol. 524, pp. 161\u2013187. Springer, Heidelberg (1991). doi:10.1007\/BFb0019974"},{"key":"16_CR20","unstructured":"Kim, H., Reich, J., Gupta, A., Shahbaz, M., Feamster, N., Clark, R.: Kinetic: verifiable dynamic network control. In: NSDI (2015)"},{"key":"16_CR21","unstructured":"Koponen, T., Amidon, K., Balland, P., Casado, M., Chanda, A., Fulton, B., Ganichev, I., Gross, J., Gude, N., Ingram, P., et al.: Network virtualization in multi-tenant datacenters. In: NSDI (2014)"},{"key":"16_CR22","unstructured":"Kuperstein, M., Vechev, M.T., Yahav, E.: Automatic inference of memory fences. In: FMCAD (2010)"},{"key":"16_CR23","doi-asserted-by":"crossref","unstructured":"Ludwig, A., Rost, M., Foucard, D., Schmid, S.: Good network updates for bad packets: waypoint enforcement beyond destination-based routing policies. In: HotNets (2014)","DOI":"10.1145\/2670518.2673873"},{"key":"16_CR24","doi-asserted-by":"crossref","unstructured":"Mart\u00ednez-Araiza, U., L\u00f3pez-Mellado, E.: CTL model repair for bounded and deadlock free petri nets. In: IFAC (2015)","DOI":"10.1016\/j.ifacol.2015.06.487"},{"key":"16_CR25","doi-asserted-by":"crossref","unstructured":"McClurg, J., Hojjat, H., Foster, N., Cerny, P.: Event-driven network programming. In: PLDI (2016)","DOI":"10.1145\/2908080.2908097"},{"key":"16_CR26","doi-asserted-by":"crossref","unstructured":"Meshman, Y., Rinetzky, N., Yahav, E.: Pattern-based synthesis of synchronization for the C++ memory model. In: FMCAD (2015)","DOI":"10.1109\/FMCAD.2015.7542261"},{"key":"16_CR27","unstructured":"Nelson, T., Ferguson, A.D., Scheer, M.J., Krishnamurthi, S.: Tierless programming and reasoning for software-defined networks. In: NSDI (2014)"},{"key":"16_CR28","doi-asserted-by":"crossref","unstructured":"Padon, O., Immerman, N., Karbyshev, A., Lahav, O., Sagiv, M., Shoham, S.: Decentralizing SDN policies. In: POPL (2015)","DOI":"10.1145\/2676726.2676990"},{"key":"16_CR29","doi-asserted-by":"crossref","unstructured":"Peres\u00edni, P., Kuzniar, M., Vasic, N., Canini, M., Kostic, D.: OF.CPP: consistent packet processing for openflow. In: HotSDN (2013)","DOI":"10.1145\/2491185.2491205"},{"key":"16_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-3-319-24953-7_4","volume-title":"Automated Technology for Verification and Analysis","author":"H Ponce-de-Le\u00f3n","year":"2015","unstructured":"Ponce-de-Le\u00f3n, H., Rodr\u00edguez, C., Carmona, J., Heljanko, K., Haar, S.: Unfolding-based process discovery. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 31\u201347. Springer, Cham (2015). doi:10.1007\/978-3-319-24953-7_4"},{"key":"16_CR31","doi-asserted-by":"crossref","unstructured":"Saha, S., Prabhu, S., Madhusudan, P.: NetGen: synthesizing data-plane configurations for network policies. In: SOSR (2015)","DOI":"10.1145\/2774993.2775006"},{"key":"16_CR32","doi-asserted-by":"crossref","unstructured":"Scott, C., Wundsam, A., Raghavan, B., Panda, A., Or, A., Lai, J., Huang, E., Liu, Z., El-Hassany, A., Whitlock, S., Acharya, H.B., Zarifis, K., Shenker, S.: Troubleshooting blackbox SDN control software with minimal causal sequences. In: SIGCOMM (2014)","DOI":"10.1145\/2619239.2626304"},{"key":"16_CR33","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Jones, C.G., Bod\u00edk, R.: Sketching concurrent data structures. In: PLDI (2008)","DOI":"10.1145\/1375581.1375599"},{"key":"16_CR34","doi-asserted-by":"crossref","unstructured":"Vechev, M., Yahav, E., Yorsh, G.: Abstraction-guided synthesis of synchronization. In: POPL (2010)","DOI":"10.1145\/1706299.1706338"},{"key":"16_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/3-540-17906-2_31","volume-title":"Petri Nets: Applications and Relationships to Other Models of Concurrency","author":"G Winskel","year":"1987","unstructured":"Winskel, G.: Event structures. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) ACPN 1986. LNCS, vol. 255, pp. 325\u2013392. Springer, Heidelberg (1987). doi:10.1007\/3-540-17906-2_31"},{"key":"16_CR36","doi-asserted-by":"crossref","unstructured":"Yuan, Y., Lin, D., Alur, R., Loo, B.T.: Scenario-based programming for SDN Policies. In: CoNEXT (2015)","DOI":"10.1145\/2716281.2836119"},{"key":"16_CR37","unstructured":"Zhou, W., Jin, D., Croft, J., Caesar, M., Godfrey, P.B.: Enforcing generalized consistency properties in software-defined networks. In: NSDI (2015)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63390-9_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,13]],"date-time":"2021-07-13T00:09:41Z","timestamp":1626134981000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-63390-9_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319633893","9783319633909"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63390-9_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"13 July 2017","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":"Heidelberg","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 July 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/cavconference.org\/2017\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}