{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,29]],"date-time":"2025-05-29T05:10:02Z","timestamp":1748495402119,"version":"3.41.0"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319216676"},{"type":"electronic","value":"9783319216683"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","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":[[2015]]},"DOI":"10.1007\/978-3-319-21668-3_23","type":"book-chapter","created":{"date-parts":[[2015,7,13]],"date-time":"2015-07-13T15:08:53Z","timestamp":1436800133000},"page":"395-412","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Automatic Completion of Distributed Protocols with Symmetry"],"prefix":"10.1007","author":[{"given":"Rajeev","family":"Alur","sequence":"first","affiliation":[]},{"given":"Mukund","family":"Raghothaman","sequence":"additional","affiliation":[]},{"given":"Christos","family":"Stergiou","sequence":"additional","affiliation":[]},{"given":"Stavros","family":"Tripakis","sequence":"additional","affiliation":[]},{"given":"Abhishek","family":"Udupa","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,14]]},"reference":[{"key":"23_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Bod\u00edk, R., Juniwal, G., Martin, M.M.K., Raghothaman, M., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-guided Synthesis. In: FMCAD, pp. 1\u201317 (2013)","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"23_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1007\/978-3-319-13338-6_7","volume-title":"Hardware and Software: Verification and Testing","author":"R Alur","year":"2014","unstructured":"Alur, R., Martin, M., Raghothaman, M., Stergiou, C., Tripakis, S., Udupa, A.: Synthesizing finite-state protocols from scenarios and requirements. In: Yahav, E. (ed.) HVC 2014. LNCS, vol. 8855, pp. 75\u201391. Springer, Heidelberg (2014)"},{"key":"23_CR3","unstructured":"Alur, R., Raghothaman, M., Stergiou, C., Tripakis, S., Udupa, A.: Automatic completion of distributed protocols with symmetry. In: CoRR, arXiv:1505.0440 (2015). http:\/\/arxiv.org\/abs\/1505.04409"},{"key":"23_CR4","doi-asserted-by":"crossref","unstructured":"Bjorner, N., Phan, A.D.: $$\\nu $$ Z - maximal satisfaction with Z3. In: Kutsia, T., Voronkov, A. (eds.) SCSS 2014. EPiC Series, vol. 30, pp. 1\u20139. EasyChair (2014)","DOI":"10.29007\/jmxj"},{"issue":"3","key":"23_CR5","doi-asserted-by":"publisher","first-page":"911","DOI":"10.1016\/j.jcss.2011.08.007","volume":"78","author":"R Bloem","year":"2012","unstructured":"Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive(1) designs. J. Comput. Syst. Sci. 78(3), 911\u2013938 (2012)","journal-title":"J. Comput. Syst. Sci."},{"key":"23_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1007\/978-3-319-10431-7_18","volume-title":"Software Engineering and Formal Methods","author":"S Cassel","year":"2014","unstructured":"Cassel, S., Howar, F., Jonsson, B., Steffen, B.: Learning extended finite state machines. In: Giannakopoulou, D., Sala\u00fcn, G. (eds.) SEFM 2014. LNCS, vol. 8702, pp. 250\u2013264. Springer, Heidelberg (2014)"},{"key":"23_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/978-3-540-30494-4_27","volume-title":"Formal Methods in Computer-Aided Design","author":"C-T Chou","year":"2004","unstructured":"Chou, C.-T., Mannava, P.K., Park, S.: A simple method for parameterized verification of cache coherence protocols. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 382\u2013398. Springer, Heidelberg (2004)"},{"key":"23_CR8","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an open-source tool for symbolic model checking. In: CAV 2002. LNCS, vol. 2404, pp. 359\u2013364. Springer, Heidelberg (2002)","DOI":"10.1007\/3-540-45657-0_29"},{"issue":"11","key":"23_CR9","doi-asserted-by":"publisher","first-page":"643","DOI":"10.1145\/361179.361202","volume":"17","author":"EW Dijkstra","year":"1974","unstructured":"Dijkstra, E.W.: Self-stabilizing Systems in spite of distributed control. Commun. ACM 17(11), 643\u2013644 (1974)","journal-title":"Commun. ACM"},{"key":"23_CR10","doi-asserted-by":"crossref","unstructured":"Dill, D.L.: The mur $$\\varphi $$ verification system. In: Proceedings of the 8th International Conference on Computer Aided Verification, pp. 390\u2013393, CAV 1996, Springer-Verlag, London, UK (1996)","DOI":"10.1007\/3-540-61474-5_86"},{"key":"23_CR11","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Havlicek, J.W., Trefler, R.J.: Virtual symmetry reduction. In: Proceedings of the Fifteenth Annual IEEE Symposium on Logic in Computer Science (LICS 2000), pp. 121\u2013131, June 2000","DOI":"10.1109\/LICS.2000.855761"},{"issue":"4","key":"23_CR12","doi-asserted-by":"publisher","first-page":"617","DOI":"10.1145\/262004.262008","volume":"19","author":"EA Emerson","year":"1997","unstructured":"Emerson, E.A., Sistla, A.P.: Utilizing symmetry when model-checking under fairness assumptions: an automata-theoretic approach. ACM Trans. Program. Lang. Syst. 19(4), 617\u2013638 (1997)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"23_CR13","doi-asserted-by":"crossref","unstructured":"Finkbeiner, B., Schewe, S.: Uniform distributed synthesis. In: IEEE Symposium on Logic in Computer Science, pp. 321\u2013330 (2005)","DOI":"10.1109\/LICS.2005.53"},{"issue":"5\u20136","key":"23_CR14","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/s10009-012-0228-z","volume":"15","author":"B Finkbeiner","year":"2013","unstructured":"Finkbeiner, B., Schewe, S.: Bounded synthesis. Softw. Tools Technol. Transf. 15(5\u20136), 519\u2013539 (2013)","journal-title":"Softw. Tools Technol. Transf."},{"key":"23_CR15","unstructured":"Gasc\u00f3n, A., Tiwari, A.: Synthesis of a simple self-stabilizing system. In: Proceedings 3rd Workshop on Synthesis, SYNT 2014, pp. 5\u201316, Vienna, Austria, July 23\u201324, 2014"},{"issue":"5","key":"23_CR16","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(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"23_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/11513988_23","volume-title":"Computer Aided Verification","author":"B Jobstmann","year":"2005","unstructured":"Jobstmann, B., Griesmayer, A., Bloem, R.: Program repair as a game. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 226\u2013238. Springer, Heidelberg (2005)"},{"key":"23_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-540-78800-3_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Katz","year":"2008","unstructured":"Katz, G., Peled, D.A.: Model checking-based genetic programming with an application to mutual exclusion. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 141\u2013156. Springer, Heidelberg (2008)"},{"key":"23_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-642-19237-1_8","volume-title":"Hardware and Software: Verification and Testing","author":"A Rich","year":"2011","unstructured":"Rich, A., Alexandron, G., Naveh, R.: An explanation-based constraint debugger. In: Namjoshi, K., Zeller, A., Ziv, A. (eds.) HVC 2009. LNCS, vol. 6405, pp. 52\u201356. Springer, Heidelberg (2011)"},{"key":"23_CR20","doi-asserted-by":"crossref","unstructured":"Lamouchi, H., Thistle, J.: Effective control synthesis for DES under partial observations. In: 39th IEEE Conference on Decision and Control, pp. 22\u201328 (2000)","DOI":"10.1109\/CDC.2000.912726"},{"key":"23_CR21","volume-title":"Distributed Algorithms","author":"NA Lynch","year":"1996","unstructured":"Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann, Burlington (1996)"},{"key":"23_CR22","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.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"issue":"1\u20132","key":"23_CR23","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/BF00625968","volume":"9","author":"IP Norris","year":"1996","unstructured":"Norris, I.P.: Better verification through symmetry. Formal Methods Syst. Des. 9(1\u20132), 41\u201375 (1996)","journal-title":"Formal Methods Syst. Des."},{"key":"23_CR24","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of the 16th ACM Symposium on Principles of Programming Languages (1989)","DOI":"10.1145\/75277.75293"},{"key":"23_CR25","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: Distributed Reactive Systems Are Hard to Synthesize. In: 31st Annual Symposium on Foundations of Computer Science. pp. 746\u2013757 (1990)","DOI":"10.1109\/FSCS.1990.89597"},{"key":"23_CR26","first-page":"81","volume":"77","author":"P Ramadge","year":"1989","unstructured":"Ramadge, P., Wonham, W.: The control of discrete event systems. IEEE Trans. Control Theory 77, 81\u201398 (1989)","journal-title":"IEEE Trans. Control Theory"},{"issue":"2","key":"23_CR27","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1145\/350887.350891","volume":"9","author":"AP Sistla","year":"2000","unstructured":"Sistla, A.P., Gyuris, V., Emerson, E.A.: SMC: a symmetry-based model checker for verification of safety and liveness properties. ACM Trans. Softw. Eng. Methodol. 9(2), 133\u2013166 (2000)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"23_CR28","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Rabbah, R., Bodik, R., Ebcioglu, K.: Programming by sketching for bit-streaming programs. In: Proceedings of the 2005 ACM Conference on Programming Language Design and Implementation (2005)","DOI":"10.1145\/1065010.1065045"},{"key":"23_CR29","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Jones, C.G., Bodik, R.: Sketching concurrent data structures. In: Proceedings of the 2008 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2008 (2008)","DOI":"10.1145\/1375581.1375599"},{"key":"23_CR30","series-title":"FMCAD 2008","first-page":"1","volume-title":"Formal Methods in Computer-Aided Design","author":"M Talupur","year":"2008","unstructured":"Talupur, M., Tuttle, M.R.: Going with the flow: parameterized verification using message flows. In: Cimatti, A., Jones, R.B. (eds.) Formal Methods in Computer-Aided Design. FMCAD 2008, pp. 1\u20138. IEEE, Portland (2008)"},{"issue":"1","key":"23_CR31","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/j.ipl.2004.01.004","volume":"90","author":"S Tripakis","year":"2004","unstructured":"Tripakis, S.: Undecidable problems of decentralized observation and control on regular languages. Inf. Process. Lett. 90(1), 21\u201328 (2004)","journal-title":"Inf. Process. Lett."},{"key":"23_CR32","doi-asserted-by":"crossref","unstructured":"Udupa, A., Raghavan, A., Deshmukh, J.V., Mador-Haim, S., Martin, M.M., Alur, R.: TRANSIT: specifying protocols with concolic snippets. In: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2013, pp. 287\u2013296 (2013)","DOI":"10.1145\/2491956.2462174"}],"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-319-21668-3_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,29]],"date-time":"2025-05-29T04:45:55Z","timestamp":1748493955000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-21668-3_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319216676","9783319216683"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21668-3_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"14 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}