{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T20:10:06Z","timestamp":1746389406703,"version":"3.40.4"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319117638"},{"type":"electronic","value":"9783319117645"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-11764-5_12","type":"book-chapter","created":{"date-parts":[[2014,9,23]],"date-time":"2014-09-23T22:53:32Z","timestamp":1411512812000},"page":"165-179","source":"Crossref","is-referenced-by-count":4,"title":["SMT-Based Synthesis of Distributed Self-stabilizing Systems"],"prefix":"10.1007","author":[{"given":"Fathiyeh","family":"Faghih","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Borzoo","family":"Bonakdarpour","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"12_CR1","unstructured":"Yices: An SMT Solver, http:\/\/yices.csl.sri.com"},{"key":"12_CR2","unstructured":"Z3: An efficient theorem prover, http:\/\/research.microsoft.com\/en-us\/um\/redmond\/projects\/z3\/"},{"issue":"1","key":"12_CR3","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/s00446-011-0139-3","volume":"25","author":"B. Bonakdarpour","year":"2012","unstructured":"Bonakdarpour, B., Kulkarni, S.S., Abujarad, F.: Symbolic synthesis of masking fault-tolerant programs. Springer Journal on Distributed Computing\u00a025(1), 83\u2013108 (2012)","journal-title":"Springer Journal on Distributed Computing"},{"issue":"1","key":"12_CR4","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"E.M. Clarke","year":"2001","unstructured":"Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods in System Design\u00a019(1), 7\u201334 (2001)","journal-title":"Formal Methods in System Design"},{"issue":"11","key":"12_CR5","doi-asserted-by":"publisher","first-page":"643","DOI":"10.1145\/361179.361202","volume":"17","author":"E.W. Dijkstra","year":"1974","unstructured":"Dijkstra, E.W.: Self-stabilizing systems in spite of distributed control. Communications of the ACM\u00a017(11), 643\u2013644 (1974)","journal-title":"Communications of the ACM"},{"issue":"1","key":"12_CR6","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/BF01843566","volume":"1","author":"E.W. Dijkstra","year":"1986","unstructured":"Dijkstra, E.W.: A belated proof of self-stabilization. Distributed Computing\u00a01(1), 5\u20136 (1986)","journal-title":"Distributed Computing"},{"key":"12_CR7","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.\u00a05799, pp. 321\u2013336. Springer, Heidelberg (2009)"},{"issue":"9","key":"12_CR8","doi-asserted-by":"publisher","first-page":"609","DOI":"10.1007\/s00236-004-0143-1","volume":"40","author":"S. Dolev","year":"2004","unstructured":"Dolev, S., Schiller, E.: Self-stabilizing group communication in directed networks. Acta Informatica\u00a040(9), 609\u2013636 (2004)","journal-title":"Acta Informatica"},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"Ebnenasir, A., Farahat, A.: A lightweight method for automated design of convergence. In: Proceedings of the 25th IEEE International Parallel and Distributed Processing Symposium (IPDPS), pp. 219\u2013230 (2011)","DOI":"10.1109\/IPDPS.2011.30"},{"key":"12_CR10","unstructured":"Emerson, E.A.: Handbook of Theoretical Computer Science. Temporal and Modal Logics, vol.\u00a0B, ch. 16. Elsevier Science Publishers B. V., Amsterdam (1990)"},{"issue":"5-6","key":"12_CR11","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. International Journal on Software Tools for Technology Transfer (STTT)\u00a015(5-6), 519\u2013539 (2013)","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"},{"issue":"2","key":"12_CR12","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1016\/0020-0190(92)90015-N","volume":"43","author":"S.-C. Hsu","year":"1992","unstructured":"Hsu, S.-C., Huang, S.-T.: A self-stabilizing algorithm for maximal matching. Information Processing Letters\u00a043(2), 77\u201381 (1992)","journal-title":"Information Processing Letters"},{"key":"12_CR13","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press Cambridge (2012)"},{"key":"12_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-642-40213-5_2","volume-title":"Fundamentals of Software Engineering","author":"A. Klinkhamer","year":"2013","unstructured":"Klinkhamer, A., Ebnenasir, A.: On the complexity of adding convergence. In: Arbab, F., Sirjani, M. (eds.) FSEN 2013. LNCS, vol.\u00a08161, pp. 17\u201333. Springer, Heidelberg (2013)"},{"key":"12_CR15","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: Proceedings of 46th Annual IEEE Symposium on Foundations of Computer Science (FOCS), pp. 531\u2013542 (2005)","DOI":"10.1109\/SFCS.2005.66"},{"issue":"14","key":"12_CR16","doi-asserted-by":"publisher","first-page":"1336","DOI":"10.1016\/j.tcs.2008.12.022","volume":"410","author":"F. Manne","year":"2009","unstructured":"Manne, F., Mjelde, M., Pilard, L., Tixeuil, S.: A new self-stabilizing maximal matching algorithm. Theoretical Computer Science\u00a0410(14), 1336\u20131345 (2009)","journal-title":"Theoretical Computer Science"},{"key":"12_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-642-33536-5_6","volume-title":"Stabilization, Safety, and Security of Distributed Systems","author":"F. Ooshita","year":"2012","unstructured":"Ooshita, F., Tixeuil, S.: On the self-stabilization of mobile oblivious robots in uniform rings. In: Richa, A.W., Scheideler, C. (eds.) SSS 2012. LNCS, vol.\u00a07596, pp. 49\u201363. Springer, Heidelberg (2012)"},{"issue":"6","key":"12_CR18","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1016\/0020-0190(94)90098-1","volume":"49","author":"G. Tel","year":"1994","unstructured":"Tel, G.: Maximal matching stabilizes in quadratic time. Information Processing Letters\u00a049(6), 271\u2013272 (1994)","journal-title":"Information Processing Letters"}],"container-title":["Lecture Notes in Computer Science","Stabilization, Safety, and Security of Distributed Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-11764-5_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T19:42:01Z","timestamp":1746387721000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-11764-5_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319117638","9783319117645"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-11764-5_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}