{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,29]],"date-time":"2025-11-29T07:52:07Z","timestamp":1764402727903,"version":"3.41.0"},"publisher-location":"Cham","reference-count":54,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319415277"},{"type":"electronic","value":"9783319415284"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"vor","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":[[2016]]},"DOI":"10.1007\/978-3-319-41528-4_9","type":"book-chapter","created":{"date-parts":[[2016,7,12]],"date-time":"2016-07-12T09:34:06Z","timestamp":1468316046000},"page":"157-176","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Synthesis of Self-Stabilising and Byzantine-Resilient Distributed Systems"],"prefix":"10.1007","author":[{"given":"Roderick","family":"Bloem","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nicolas","family":"Braud-Santoni","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Swen","family":"Jacobs","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,7,13]]},"reference":[{"key":"9_CR1","unstructured":"Alur, R., Bodik, R., Juniwal, G., Martin, M.M., Raghothaman, M., Seshia, S., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A., et al.: Syntax-guided synthesis. In: Formal Methods in Computer-Aided Design (FMCAD), 2013, pp. 1\u20138. IEEE (2013)"},{"key":"9_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-642-54013-4_15","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"B Aminof","year":"2014","unstructured":"Aminof, B., Jacobs, S., Khalimov, A., Rubin, S.: Parameterized model checking of token-passing systems. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 262\u2013281. Springer, Heidelberg (2014). http:\/\/doai.io\/10.1007\/978-3-642-54013-4_15"},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1007\/978-3-662-49122-5_23","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S Au\u00dferlechner","year":"2016","unstructured":"Au\u00dferlechner, S., Jacobs, S., Khalimov, A.: Tight cutoffs for guarded protocols with fairness. In: Jobstmann, B., et al. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 476\u2013494. Springer, Heidelberg (2016). doi: 10.1007\/978-3-662-49122-5_23"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-642-28756-5_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Babiak","year":"2012","unstructured":"Babiak, T., K\u0159et\u00ednsk\u00fd, M., \u0158eh\u00e1k, V., Strej\u010dek, J.: LTL to B\u00fcchi automata translation: fast and more deterministic. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 95\u2013109. Springer, Heidelberg (2012). http:\/\/doai.io\/10.1007\/978-3-642-28756-5_8"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-540-73368-3_34","volume-title":"Computer Aided Verification","author":"CW Barrett","year":"2007","unstructured":"Barrett, C.W., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 298\u2013302. Springer, Heidelberg (2007)"},{"issue":"3","key":"9_CR6","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/s00236-013-0191-5","volume":"51","author":"R Bloem","year":"2014","unstructured":"Bloem, R., Chatterjee, K., Greimel, K., Henzinger, T., Hofferek, G., Jobstmann, B., K\u00f6nighofer, B., K\u00f6nighofer, R.: Synthesizing robust systems. Acta Informatica 51(3), 193\u2013220 (2014). http:\/\/doai.io\/10.1007\/s00236-013-0191-5","journal-title":"Acta Informatica"},{"key":"9_CR7","series-title":"Synthesis Lectures on Distributed Computing Theory","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-031-02011-7","volume-title":"Decidability of Parameterized Verification","author":"R Bloem","year":"2015","unstructured":"Bloem, R., Jacobs, S., Khalimov, A., Konnov, I., Rubin, S., Veith, H., Widder, J.: Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, San Rafael (2015). http:\/\/doai.io\/10.2200\/S00658ED1V01Y201508DCT013"},{"issue":"3","key":"9_CR8","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). http:\/\/doai.io\/10.1016\/j.jcss.2011.08.007","journal-title":"J. Comput. Syst. Sci."},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Bollig, B.: Logic for communicating automata with parameterized topology. In: CSL-LICS, pp. 18:1\u201318:10. ACM (2014)","DOI":"10.1145\/2603088.2603093"},{"key":"9_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2011","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70\u201387. Springer, Heidelberg (2011). http:\/\/doai.io\/10.1007\/978-3-642-18275-4_7"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/3-540-44987-6_17","volume-title":"Advances in Cryptology - EUROCRYPT 2001","author":"R Canetti","year":"2001","unstructured":"Canetti, R., Damgrd, I., Dziembowski, S., Ishai, Y., Malkin, T.: On adaptive vs. non-adaptive security of multiparty protocols. In: Pfitzmann, B. (ed.) EUROCRYPT 2001. LNCS, vol. 2045, pp. 262\u2013279. Springer, Heidelberg (2001)"},{"key":"9_CR12","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). http:\/\/doai.io\/10.1007\/978-3-642-39799-8_68"},{"issue":"11","key":"9_CR13","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":"9_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/978-3-642-04761-9_24","volume-title":"Automated Technology for Verification and Analysis","author":"R Dimitrova","year":"2009","unstructured":"Dimitrova, R., Finkbeiner, B.: Synthesis of fault-tolerant distributed systems. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 321\u2013336. Springer, Heidelberg (2009). http:\/\/doai.io\/10.1007\/978-3-642-04761-9_24"},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-319-03089-0_17","volume-title":"Stabilization, Safety, and Security of Distributed Systems","author":"D Dolev","year":"2013","unstructured":"Dolev, D., Korhonen, J.H., Lenzen, C., Rybicki, J., Suomela, J.: Synchronous counting and computational algorithm design. In: Higashino, T., Katayama, Y., Masuzawa, T., Potop-Butucaru, M., Yamashita, M. (eds.) SSS 2013. LNCS, vol. 8255, pp. 237\u2013250. Springer, Heidelberg (2013). http:\/\/doai.io\/10.1007\/978-3-319-03089-0_17"},{"key":"9_CR16","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/6156.001.0001","volume-title":"Self-Stabilization","author":"S Dolev","year":"2000","unstructured":"Dolev, S.: Self-Stabilization. MIT Press, Cambridge (2000)"},{"issue":"5","key":"9_CR17","doi-asserted-by":"publisher","first-page":"780","DOI":"10.1145\/1017460.1017463","volume":"51","author":"S Dolev","year":"2004","unstructured":"Dolev, S., Welch, J.L.: Self-stabilizing clock synchronization in the presence of Byzantine faults. J. ACM (JACM) 51(5), 780\u2013799 (2004)","journal-title":"J. ACM (JACM)"},{"issue":"1","key":"9_CR18","doi-asserted-by":"crossref","first-page":"400","DOI":"10.1145\/2914770.2837650","volume":"51","author":"Cezara Dr\u0103goi","year":"2016","unstructured":"Dragoi, C., Henzinger, T.A., Zufferey, D.: PSync: a partially synchronous language for fault-tolerant distributed algorithms. In: POPL, pp. 400\u2013415. ACM (2016). http:\/\/doai.io\/10.1145\/2837614.2837650","journal-title":"ACM SIGPLAN Notices"},{"issue":"4","key":"9_CR19","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1142\/S0129054103001881","volume":"14","author":"EA Emerson","year":"2003","unstructured":"Emerson, E.A., Namjoshi, K.S.: On reasoning about rings. Int. J. Found. Comput. Sci. 14(4), 527\u2013550 (2003). http:\/\/doai.io\/10.1142\/S0129054103001881","journal-title":"Int. J. Found. Comput. Sci."},{"key":"9_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/10721959_19","volume-title":"Automated Deduction - CADE-17","author":"E Emerson","year":"2000","unstructured":"Emerson, E., Kahlon, V.: Reducing model checking of the many to the few. In: McAllester, D. (ed.) Automated Deduction - CADE-17. LNCS, vol. 1831, pp. 236\u2013254. Springer, Berlin Heidelberg (2000)"},{"issue":"3","key":"9_CR21","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1145\/2767133","volume":"10","author":"F Faghih","year":"2015","unstructured":"Faghih, F., Bonakdarpour, B.: SMT-based synthesis of distributed self-stabilizing systems. TAAS 10(3), 21 (2015). http:\/\/doai.io\/10.1145\/2767133","journal-title":"TAAS"},{"key":"9_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/978-3-642-27940-9_15","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"B Finkbeiner","year":"2012","unstructured":"Finkbeiner, B., Jacobs, S.: Lazy synthesis. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 219\u2013234. Springer, Heidelberg (2012)"},{"key":"9_CR23","unstructured":"Finkbeiner, B., Schewe, S.: Uniform distributed synthesis. In: (LICS 2005), pp. 321\u2013330. IEEE Computer Society (2005). http:\/\/doai.io\/10.1109\/LICS.2005.53"},{"issue":"5\u20136","key":"9_CR24","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. STTT 15(5\u20136), 519\u2013539 (2013). http:\/\/doai.io\/10.1007\/s10009-012-0228-z","journal-title":"STTT"},{"issue":"2","key":"9_CR25","doi-asserted-by":"publisher","first-page":"374","DOI":"10.1145\/3149.214121","volume":"32","author":"MJ Fischer","year":"1985","unstructured":"Fischer, M.J., Lynch, N.A., Paterson, M.: Impossibility of distributed consensus with one faulty process. J. ACM 32(2), 374\u2013382 (1985). http:\/\/doai.io\/10.1145\/3149.214121","journal-title":"J. ACM"},{"key":"9_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-540-27813-9_14","volume-title":"Computer Aided Verification","author":"H Ganzinger","year":"2004","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): fast decision procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 175\u2013188. Springer, Heidelberg (2004). http:\/\/doai.io\/10.1007\/978-3-540-27813-9_14"},{"issue":"3","key":"9_CR27","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"SM German","year":"1992","unstructured":"German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM 39(3), 675\u2013735 (1992)","journal-title":"J. ACM"},{"key":"9_CR28","doi-asserted-by":"crossref","unstructured":"Hawblitzel, C., Howell, J., Kapritsos, M., Lorch, J.R., Parno, B., Roberts, M.L., Setty, S.T.V., Zill, B.: Ironfleet: proving practical distributed systems correct. In: SOSP, pp. 1\u201317. ACM (2015)","DOI":"10.1145\/2815400.2815428"},{"key":"9_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/978-3-642-02658-4_29","volume-title":"Computer Aided Verification","author":"S Jacobs","year":"2009","unstructured":"Jacobs, S.: Incremental instance generation in local reasoning. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 368\u2013382. Springer, Heidelberg (2009)"},{"key":"9_CR30","unstructured":"Jacobs, S., Bloem, R.: Parameterized synthesis. Log. Methods Comput. Sci. 10, 1\u201329 (2014). http:\/\/arxiv.org\/abs\/1401.3588"},{"key":"9_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-642-31612-8_10","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"M Janota","year":"2012","unstructured":"Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.: Solving QBF with counterexample guided refinement. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 114\u2013128. Springer, Heidelberg (2012)"},{"key":"9_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"928","DOI":"10.1007\/978-3-642-39799-8_66","volume-title":"Computer Aided Verification","author":"A Khalimov","year":"2013","unstructured":"Khalimov, A., Jacobs, S., Bloem, R.: PARTY parameterized synthesis of token rings. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 928\u2013933. Springer, Heidelberg (2013)"},{"key":"9_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-642-35873-9_9","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Khalimov","year":"2013","unstructured":"Khalimov, A., Jacobs, S., Bloem, R.: Towards efficient parameterized synthesis. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 108\u2013127. Springer, Heidelberg (2013)"},{"key":"9_CR34","doi-asserted-by":"crossref","unstructured":"K\u00f6ksal, A.S., Pu, Y., Srivastava, S., Bod\u00edk, R., Fisher, J., Piterman, N.: Synthesis of biological models from mutation experiments. In: POPL, pp. 469\u2013482. ACM (2013)","DOI":"10.1145\/2480359.2429125"},{"key":"9_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-319-21690-4_6","volume-title":"Computer Aided Verification","author":"I Konnov","year":"2015","unstructured":"Konnov, I., Veith, H., Widder, J.: SMT and POR beat counter abstraction: parameterized model checking of threshold-based distributed algorithms. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 85\u2013102. Springer, Heidelberg (2015). http:\/\/doai.io\/10.1007\/978-3-319-21690-4_6"},{"issue":"5\u20136","key":"9_CR36","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1007\/s10009-011-0217-7","volume":"15","author":"V Kuncak","year":"2013","unstructured":"Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Functional synthesis for linear arithmetic and sets. STTT 15(5\u20136), 455\u2013474 (2013). http:\/\/doai.io\/10.1007\/s10009-011-0217-7","journal-title":"STTT"},{"key":"9_CR37","unstructured":"Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: FOCS 2005, pp. 531\u2013542. IEEE Computer Society (2005). http:\/\/doai.io\/10.1109\/SFCS.2005.66"},{"issue":"3","key":"9_CR38","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1145\/357172.357176","volume":"4","author":"L Lamport","year":"1982","unstructured":"Lamport, L., Shostak, R., Pease, M.: The Byzantine generals problem. ACM Trans. Program. Lang. Syst. 4(3), 382\u2013401 (1982). http:\/\/doai.io\/10.1145\/357172.357176","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-642-24100-0_10","volume-title":"Distributed Computing","author":"L Lamport","year":"2011","unstructured":"Lamport, L.: Brief announcement: leaderless Byzantine paxos. In: Peleg, D. (ed.) Distributed Computing. LNCS, vol. 6950, pp. 141\u2013142. Springer, Heidelberg (2011)"},{"key":"9_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/3-540-45657-0_19","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2002","unstructured":"McMillan, K.L.: Applying SAT methods in unbounded symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 250\u2013264. Springer, Heidelberg (2002). http:\/\/doai.io\/10.1007\/3-540-45657-0_19"},{"key":"9_CR41","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-540-73595-3_13","volume-title":"Automated Deduction \u2013 CADE-21","author":"L de Moura","year":"2007","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Efficient e-matching for SMT solvers. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 183\u2013198. Springer, Heidelberg (2007)"},{"key":"9_CR42","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 de Moura","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). http:\/\/doai.io\/10.1007\/978-3-540-78800-3_24"},{"issue":"2","key":"9_CR43","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1145\/322186.322188","volume":"27","author":"M Pease","year":"1980","unstructured":"Pease, M., Shostak, R., Lamport, L.: Reaching agreement in the presence of faults. J. ACM 27(2), 228\u2013234 (1980)","journal-title":"J. ACM"},{"key":"9_CR44","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: Distributed reactive systems are hard to synthesize. In: 2013 IEEE 54th Annual Symposium on Foundations of Computer Science 1990, vol. 2, pp. 746\u2013757 (1990)","DOI":"10.1109\/FSCS.1990.89597"},{"key":"9_CR45","unstructured":"Qadir, J., Hasan, O.: Applying formal methods to networking: Theory, techniques and applications. CoRR abs\/1311.4303 (2013). http:\/\/arxiv.org\/abs\/1311.4303"},{"key":"9_CR46","unstructured":"Saissi, H., Bokor, P., Muftuoglu, C.A., Suri, N., Serafini, M.: Efficient verification of distributed protocols using stateful model checking. In: SRDS, pp. 133\u2013142. IEEE (2013). http:\/\/doai.io\/10.1109\/SRDS.2013.22"},{"issue":"5","key":"9_CR47","doi-asserted-by":"publisher","first-page":"1449","DOI":"10.1137\/S0097539796307698","volume":"29","author":"ME Saks","year":"2000","unstructured":"Saks, M.E., Zaharoglou, F.: Wait-free k-set agreement is impossible: the topology of public knowledge. SIAM J. Comput. 29(5), 1449\u20131483 (2000). http:\/\/doai.io\/10.1137\/S0097539796307698","journal-title":"SIAM J. Comput."},{"issue":"4","key":"9_CR48","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1016\/j.ipl.2013.11.012","volume":"114","author":"S Schewe","year":"2014","unstructured":"Schewe, S.: Distributed synthesis is simply undecidable. Inf. Process. Lett. 114(4), 203\u2013207 (2014). http:\/\/doai.io\/10.1016\/j.ipl.2013.11.012","journal-title":"Inf. Process. Lett."},{"key":"9_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"444","DOI":"10.1007\/BFb0028580","volume-title":"STACS 98","author":"T Schwentick","year":"1998","unstructured":"Schwentick, T., Barthelmann, K.: Local norms forms for first-order logic with applications to games and automata. In: Meinel, C., Morvan, M. (eds.) STACS 1998. LNCS, vol. 1373, pp. 444\u2013454. Springer, Heidelberg (1998)"},{"key":"9_CR50","unstructured":"Sickert, S.: Converting linear temporal logic to deterministic (generalised) rabin automata. Archive of Formal Proofs 2015 (2015)"},{"key":"9_CR51","unstructured":"Solar Lezama, A.: Program synthesis by sketching. Ph.D. thesis, EECS Department, University of California, Berkeley (2008). http:\/\/www.eecs.berkeley.edu\/Pubs\/TechRpts\/2008\/EECS-2008-177.html"},{"issue":"11","key":"9_CR52","doi-asserted-by":"crossref","first-page":"404","DOI":"10.1145\/1168918.1168907","volume":"41","author":"Armando Solar-Lezama","year":"2006","unstructured":"Solar-Lezama, A., Tancau, L., Bod\u00edk, R., Seshia, S.A., Saraswat, V.A.: Combinatorial sketching for finite programs. In: ASPLOS 2006, pp. 404\u2013415. ACM (2006). http:\/\/doai.io\/10.1145\/1168857.1168907","journal-title":"ACM SIGPLAN Notices"},{"key":"9_CR53","doi-asserted-by":"crossref","unstructured":"Tixeuil, S.: Self-stabilizing algorithms. In: Algorithms and Theory of Computation Handbook. Applied Algorithms and Data Structures, 2nd edn, pp. 26.1\u201326.45. Chapman & Hall\/CRC, CRC Press, Taylor & Francis Group (2009)","DOI":"10.1201\/9781584888215-c26"},{"key":"9_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/978-3-642-00768-2_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Vechev","year":"2009","unstructured":"Vechev, M., Yahav, E., Yorsh, G.: Inferring synchronization under limited observability. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 139\u2013154. Springer, Heidelberg (2009). http:\/\/doai.io\/10.1007\/978-3-642-00768-2_13"}],"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-41528-4_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,4]],"date-time":"2025-06-04T00:41:25Z","timestamp":1748997685000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-41528-4_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319415277","9783319415284"],"references-count":54,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-41528-4_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"13 July 2016","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":"Toronto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 July 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 July 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}