{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:25:11Z","timestamp":1740122711314,"version":"3.37.3"},"reference-count":55,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2016,4,1]],"date-time":"2016-04-01T00:00:00Z","timestamp":1459468800000},"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":["Form Methods Syst Des"],"published-print":{"date-parts":[[2016,4]]},"DOI":"10.1007\/s10703-016-0252-9","type":"journal-article","created":{"date-parts":[[2016,6,29]],"date-time":"2016-06-29T09:19:42Z","timestamp":1467191982000},"page":"94-147","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Synthesis of large dynamic concurrent programs from dynamic specifications"],"prefix":"10.1007","volume":"48","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1989-0974","authenticated-orcid":false,"given":"Paul C.","family":"Attie","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,6,28]]},"reference":[{"key":"252_CR1","doi-asserted-by":"crossref","unstructured":"Almagor S, Kupferman O (2014) Latticed-ltl synthesis in the presence of noisy inputs. In: Muscholl A (ed) Foundations of software science and computation structures - 17th international conference, FOSSACS 2014, held as part of the European joint conferences on theory and practice of software, ETAPS 2014, Grenoble, France, April 5\u201313, 2014. Proceedings, lecture notes in computer science, vol 8412. Springer, Berlin, pp 226\u2013241","DOI":"10.1007\/978-3-642-54830-7_15"},{"key":"252_CR2","doi-asserted-by":"crossref","unstructured":"Anuchitanukul A, Manna Z (1994) Realizability and synthesis of reactive modules. In: Proceedings of the 6th international conference on computer aided verification. Lecture notes in computer science, vol 818. Springer, Berlin, pp 156\u2013169","DOI":"10.1007\/3-540-58179-0_51"},{"key":"252_CR3","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-2714-2","volume-title":"Verification of sequential and concurrent programs","author":"K Apt","year":"1997","unstructured":"Apt K, Olderog E (1997) Verification of sequential and concurrent programs. Springer, Berlin"},{"key":"252_CR4","doi-asserted-by":"crossref","unstructured":"Arons T, Pnueli A, Ruah S, Xu J, Zuck L (2001) Parameterized verification with automatically computed inductive assertions. In: CAV","DOI":"10.1007\/3-540-44585-4_19"},{"key":"252_CR5","doi-asserted-by":"crossref","unstructured":"Attie PC, Bensalem S, Bozga M, Jaber M, Sifakis J, Zaraket FA (2013) An abstract framework for deadlock prevention in BIP. In: Beyer D, Boreale M (eds) Formal techniques for distributed systems\u2014joint IFIP WG 6.1 international conference, FMOODS\/FORTE 2013, held as part of the 8th international federated conference on distributed computing techniques, DisCoTec 2013, Florence, Italy, June 3\u20135, 2013, proceedings. Lecture notes in computer science, vol 7892. Springer, Berlin, pp 161\u2013177","DOI":"10.1007\/978-3-642-38592-6_12"},{"key":"252_CR6","doi-asserted-by":"crossref","unstructured":"Attie PC, Cherri A, Bab KDA, Sakr M, Saklawi J (2015) Model and program repair via SAT solving. In: 13. ACM\/IEEE international conference on formal methods and models for codesign, MEMOCODE 2015, Austin, TX, USA, September 21\u201323, 2015. IEEE, pp 148\u2013157. Tool download available at http:\/\/eshmuntool.blogspot.com\/","DOI":"10.1109\/MEMCOD.2015.7340481"},{"key":"252_CR7","unstructured":"Attie PC, Emerson EA (2001) Synthesis of concurrent systems for an atomic read\/write model of computation. ACM Trans Program Lang Syst 23(2):187\u2013242. Extended abstract appears in proceedings of the 15\u2019th ACM symposium of principles of distributed computing (PODC), Philadelphia, May 1996, pp 111\u2013120"},{"key":"252_CR8","doi-asserted-by":"crossref","unstructured":"Attie PC, Lynch N. (2016) Dynamic input\/output automata: a formal and compositional model for dynamic systems. Information and Computation","DOI":"10.1016\/j.ic.2016.03.008"},{"key":"252_CR9","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.tcs.2015.11.032","volume":"619","author":"PC Attie","year":"2016","unstructured":"Attie PC (2016) Finite-state concurrent programs can be expressed in pairwise normal form. Theor Comput Sci 619:1\u201331","journal-title":"Theor Comput Sci"},{"key":"252_CR10","doi-asserted-by":"crossref","unstructured":"Attie P, Arora A, Emerson EA (2004) Synthesis of fault-tolerant concurrent programs. ACM Trans Program Lang Syst 26(1):125\u2013185. Extended abstract appears in proceedings of the 17\u2019th ACM symposium of principles of distributed computing (PODC), Puerto Vallarta, Mexico, pp 173\u2013182","DOI":"10.1145\/963778.963782"},{"key":"252_CR11","doi-asserted-by":"crossref","unstructured":"Attie P, Chockler H (2005) Efficiently verifiable conditions for deadlock-freedom of large concurrent programs. In: Proceedings of VMCAI 2005: verification, model checking and abstract interpretation, Paris","DOI":"10.1007\/978-3-540-30579-8_30"},{"issue":"1","key":"252_CR12","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1145\/271510.271519","volume":"20","author":"PC Attie","year":"1998","unstructured":"Attie PC, Emerson EA (1998) Synthesis of concurrent systems with many similar processes. ACM Trans Program Lang Syst 20(1):51\u2013115. doi: 10.1145\/271510.271519","journal-title":"ACM Trans Program Lang Syst"},{"key":"252_CR13","doi-asserted-by":"crossref","unstructured":"Avni G, Kupferman O (2014) Synthesis from component libraries with costs. In: Baldan P, Gorla D (eds) CONCUR 2014\u2014concurrency theory\u201425th international conference, CONCUR 2014, Rome, Italy, September 2\u20135, 2014. Proceedings, lecture notes in computer science, vol 8704. Springer, Berlin, pp 156\u2013172","DOI":"10.1007\/978-3-662-44584-6_12"},{"key":"252_CR14","doi-asserted-by":"crossref","unstructured":"Bloem R, Jacobs S, Khalimov A, Konnov I, Rubin S, Veith H, Widder J (2015) Decidability of parameterized verification. Synthesis lectures on distributed computing theory. Morgan & Claypool Publishers, San Rafael","DOI":"10.2200\/S00658ED1V01Y201508DCT013"},{"key":"252_CR15","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1145\/1879021.1879049","volume-title":"EMSOFT","author":"B Bonakdarpour","year":"2010","unstructured":"Bonakdarpour B, Bozga M, Jaber M, Quilbeuf J, Sifakis J (2010) From high-level component-based models to distributed implementations. In: Carloni CP, Tripakis S (eds) EMSOFT. ACM, New York, pp 209\u2013218"},{"issue":"5","key":"252_CR16","doi-asserted-by":"crossref","first-page":"383","DOI":"10.1007\/s00446-012-0168-6","volume":"25","author":"B Bonakdarpour","year":"2012","unstructured":"Bonakdarpour B, Bozga M, Jaber M, Quilbeuf J, Sifakis J (2012) A framework for automated distributed implementation of component-based models. Distrib Comput 25(5):383\u2013409","journal-title":"Distrib Comput"},{"issue":"1","key":"252_CR17","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1007\/s00446-011-0139-3","volume":"25","author":"B Bonakdarpour","year":"2012","unstructured":"Bonakdarpour B, Kulkarni S, Abujarad F (2012) Symbolic synthesis of masking fault-tolerant distributed programs. Distrib Comput 25(1):83\u2013108","journal-title":"Distrib Comput"},{"key":"252_CR18","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/0304-3975(88)90098-9","volume":"59","author":"M Browne","year":"1988","unstructured":"Browne M, Clarke EM, Grumberg O (1988) Characterizing finite kripke structures in propositional temporal logic. Theor Comput Sci 59:115\u2013131","journal-title":"Theor Comput Sci"},{"issue":"1","key":"252_CR19","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1016\/S0004-3702(99)00039-9","volume":"112","author":"F Buccafurri","year":"1999","unstructured":"Buccafurri F, Eiter T, Gottlob G, Leone N (1999) Enhancing model checking in verification by AI techniques. Artif Intell 112(1):57\u2013104","journal-title":"Artif Intell"},{"issue":"3","key":"252_CR20","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2168\/LMCS-11(3:11)2015","volume":"11","author":"G Chatzieleftheriou","year":"2015","unstructured":"Chatzieleftheriou G, Bonakdarpour B, Katsaros P, Smolka SA (2015) Abstract model repair. Log Methods Comput Sci 11(3):1\u201343","journal-title":"Log Methods Comput Sci"},{"key":"252_CR21","doi-asserted-by":"crossref","unstructured":"Clarke EM, Emerson EA, Sistla P (1986) Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans Program Lang Syst 8(2):244\u2013263. Extended abstract in proceedings of the 10th annual ACM symposium on principles of programming languages","DOI":"10.1145\/5397.5399"},{"key":"252_CR22","doi-asserted-by":"crossref","unstructured":"Clarke EM, Grumberg O, Browne MC (1986) Reasoning about networks with many identical finite-state processes. In: Proceedings of the 5th annual ACM symposium on principles of distributed computing. ACM, New York, pp 240\u2013248","DOI":"10.1145\/10590.10611"},{"key":"252_CR23","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura LM, Owre S, Rue\u00df H, Rushby JM, Shankar N, Sorea M, Tiwari A (2004) SAL 2. In: Alur R, Peled DA (eds) Computer aided verification, 16th international conference, CAV 2004, Boston, MA, USA, July 13\u201317, 2004. Proceedings, lecture notes in computer science, vol 3114. Springer, Berlin, pp 496\u2013500","DOI":"10.1007\/978-3-540-27813-9_45"},{"key":"252_CR24","doi-asserted-by":"crossref","unstructured":"Deng X, Dwyer MB, Hatcliff J, Mizuno M (2002) Invariant-based specification, synthesis, and verification of synchronization in concurrent programs. In: Proceedings of the 24th international conference on software engineering, ICSE \u201902. ACM, New York, pp 442\u2013452","DOI":"10.1145\/581339.581394"},{"issue":"11","key":"252_CR25","doi-asserted-by":"crossref","first-page":"643","DOI":"10.1145\/361179.361202","volume":"17","author":"EW Dijkstra","year":"1974","unstructured":"Dijkstra EW (1974) Self-stabilizing systems in spite of distributed control. Commun ACM 17(11):643\u2013644","journal-title":"Commun ACM"},{"key":"252_CR26","volume-title":"A discipline of programming","author":"EW Dijkstra","year":"1976","unstructured":"Dijkstra EW (1976) A discipline of programming. Prentice-Hall Inc., Englewood Cliffs"},{"key":"252_CR27","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-5695-3","volume-title":"Selected writings on computing: a personal perspective","author":"EW Dijkstra","year":"1982","unstructured":"Dijkstra EW (1982) Selected writings on computing: a personal perspective. Springer, New York"},{"key":"252_CR28","unstructured":"Dill D, Wong-Toi H (1990) Synthesizing processes and schedulers from temporal specifications. In: International conference on computer-aided verification, no. 531 in LNCS. Springer, Berlin, pp 272\u2013281"},{"key":"252_CR29","doi-asserted-by":"crossref","unstructured":"Emerson EA (1990) Temporal and modal logic. In: Leeuwen JV (ed) Handbook of theoretical computer science. Formal models and semantics, vol B. The MIT Press, Cambridge","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"252_CR30","doi-asserted-by":"crossref","unstructured":"Emerson EA, Kahlon V (2000) Reducing model checking of the many to the few. In: Conference on automated deduction, pp 236\u2013254","DOI":"10.1007\/10721959_19"},{"key":"252_CR31","unstructured":"Emerson EA, Namjoshi KS (1996) Automatic verification of parameterized synchronous systems (extended abstract). In: CAV, pp 87\u201398"},{"key":"252_CR32","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"EA Emerson","year":"1982","unstructured":"Emerson EA, Clarke EM (1982) Using branching time temporal logic to synthesize synchronization skeletons. Sci Comput Program 2:241\u2013266","journal-title":"Sci Comput Program"},{"key":"252_CR33","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1016\/0167-6423(87)90036-0","volume":"8","author":"EA Emerson","year":"1987","unstructured":"Emerson EA, Lei C (1987) Modalities for model checking: branching time logic strikes back. Sci Comput Program 8:275\u2013306","journal-title":"Sci Comput Program"},{"key":"252_CR34","doi-asserted-by":"crossref","unstructured":"Faghih F, Bonakdarpour B (2014) SMT-based synthesis of distributed self-stabilizing systems. In: Felber P, Garg VK (eds) Stabilization, safety, and security of distributed systems\u201416th international symposium, SSS 2014, Paderborn, Germany, September 28\u2013October 1, 2014. Proceedings, lecture notes in computer science, vol 8756. Springer, Berlin, pp 165\u2013179","DOI":"10.1007\/978-3-319-11764-5_12"},{"key":"252_CR35","doi-asserted-by":"crossref","unstructured":"Fekete A, Gupta D, Luchango V, Lynch N, Shvartsman A (1999) Eventually-serializable data services. Theor Comput Sci 220:113\u2013156. Conference version appears in ACM symposium on principles of distributed computing, 1996","DOI":"10.1016\/S0304-3975(98)00239-4"},{"issue":"5\u20136","key":"252_CR36","doi-asserted-by":"crossref","first-page":"519","DOI":"10.1007\/s10009-012-0228-z","volume":"15","author":"B Finkbeiner","year":"2013","unstructured":"Finkbeiner B, Schewe S (2013) Bounded synthesis. Int J Softw ToolsTechnol Transf 15(5\u20136):519\u2013539","journal-title":"Int J Softw ToolsTechnol Transf"},{"key":"252_CR37","doi-asserted-by":"crossref","unstructured":"Gasc\u00f3n A, Tiwari A (2014) Synthesis of a simple self-stabilizing system. In: Chatterjee K, Ehlers R, Jha S (eds) Proceedings 3rd workshop on synthesis, SYNT 2014, Vienna, Austria, July 23\u201324, 2014. EPTCS, vol 157, pp 5\u201316","DOI":"10.4204\/EPTCS.157.5"},{"issue":"3","key":"252_CR38","doi-asserted-by":"crossref","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O Grumberg","year":"1994","unstructured":"Grumberg O, Long D (1994) Model checking and modular verification. ACM Trans Program Lang Syst 16(3):843\u2013871","journal-title":"ACM Trans Program Lang Syst"},{"issue":"10","key":"252_CR39","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare CAR (1969) An axiomatic basis for computer programming. Commun ACM 12(10):576\u2013580 583","journal-title":"Commun ACM"},{"key":"252_CR40","doi-asserted-by":"crossref","unstructured":"Kupferman O, Madhusudan P, Thiagarajan P, Vardi M (2000) Open systems in reactive environments: control and synthesis. In: Proceedings of the 11th international conference on concurrency theory, lecture notes in computer science, vol 1877. Springer, Berlin, pp 92\u2013107","DOI":"10.1007\/3-540-44618-4_9"},{"key":"252_CR41","unstructured":"Kupferman O, Vardi M (1997) Synthesis with incomplete information. In: 2nd international conference on temporal logic, Manchester, pp 91\u2013106"},{"issue":"4","key":"252_CR42","doi-asserted-by":"crossref","first-page":"360","DOI":"10.1145\/138873.138877","volume":"10","author":"R Ladin","year":"1992","unstructured":"Ladin R, Liskov B, Shrira L, Ghemawat S (1992) Providing high availability using lazy replication. ACM Trans Comput Syst 10(4):360\u2013391","journal-title":"ACM Trans Comput Syst"},{"key":"252_CR43","volume-title":"Program development in java","author":"B Liskov","year":"2001","unstructured":"Liskov B (2001) Program development in java. Addison Wesley, Reading"},{"key":"252_CR44","doi-asserted-by":"crossref","unstructured":"Lustig Y, Vardi MY (2009) Synthesis from component libraries. In: Proceedings of the 12th international conference on foundations of software science and computational structures: held as part of the joint European conferences on theory and practice of software. ETAPS 2009, FOSSACS \u201909. Springer, Berlin, pp 395\u2013409","DOI":"10.1007\/978-3-642-00596-1_28"},{"key":"252_CR45","volume-title":"Distribiuted algorithms","author":"NA Lynch","year":"1996","unstructured":"Lynch NA (1996) Distribiuted algorithms. Morgan Kaufmann, Burlington"},{"key":"252_CR46","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal verification of reactive systems\u2014safety","author":"Z Manna","year":"1995","unstructured":"Manna Z, Pnueli A (1995) Temporal verification of reactive systems\u2014safety. Springer, Berlin"},{"key":"252_CR47","doi-asserted-by":"crossref","unstructured":"Manna Z, Wolper P (1984) Synthesis of communicating processes from temporal logic specifications. ACM Trans Program Lang Syst 6(1):68\u201393. Also appears in proceedings of the workshop on logics of programs, Yorktown-Heights, NY. Lecture notes in computer science, vol 131. Springer, Berlin","DOI":"10.1145\/357233.357237"},{"key":"252_CR48","doi-asserted-by":"crossref","unstructured":"Pnueli A, Rosner R (1989) On the synthesis of a reactive module. In: Proceedings of the 16th ACM symposium on principles of programming languages. ACM, New York, pp 179\u2013190","DOI":"10.1145\/75277.75293"},{"key":"252_CR49","doi-asserted-by":"crossref","unstructured":"Pnueli A, Rosner R (1989) On the synthesis of asynchronous reactive modules. In: Proceedings of the 16th ICALP. Lecture notes in computer science, vol 372. Springer, Berlin, pp 652\u2013671","DOI":"10.1007\/BFb0035790"},{"key":"252_CR50","doi-asserted-by":"crossref","unstructured":"Pnueli A, Ruah S, Zuck L (2001) Automatic deductive verification with invisible invariants. In: TACAS","DOI":"10.1007\/3-540-45319-9_7"},{"key":"252_CR51","doi-asserted-by":"crossref","unstructured":"Schewe S, Finkbeiner B (2007) Bounded synthesis. In: Namjoshi KS, Yoneda T, Higashino T, Okamura Y (eds) Automated technology for verification and analysis, 5th international symposium, ATVA 2007, Tokyo, Japan, October 22\u201325, 2007. Proceedings, lecture notes in computer science, vol 4762. Springer, Berlin, pp 474\u2013488","DOI":"10.1007\/978-3-540-75596-8_33"},{"key":"252_CR52","volume-title":"Verification of sequential and concurrent programs","author":"F Schneider","year":"1997","unstructured":"Schneider F (1997) Verification of sequential and concurrent programs. Springer, Berlin"},{"key":"252_CR53","unstructured":"Sistla AP, German SM (1992) Reasoning about systems with many processes. J ACM 39(3):675\u2013735. Conference version appears in IEEE logic in computer science 1987"},{"issue":"2","key":"252_CR54","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"R Tarjan","year":"1972","unstructured":"Tarjan R (1972) Depth-first search and linear graph algorithms. SIAM J Comput 1(2):146\u2013160","journal-title":"SIAM J Comput"},{"key":"252_CR55","doi-asserted-by":"crossref","unstructured":"Wolper P (1986) Expressing interesting properties of programs in propositional temporal logic. In: Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on principles of programming languages. POPL \u201986. ACM, New York, pp 184\u2013193","DOI":"10.1145\/512644.512661"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-016-0252-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-016-0252-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-016-0252-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,10]],"date-time":"2019-09-10T06:54:23Z","timestamp":1568098463000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-016-0252-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,4]]},"references-count":55,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2016,4]]}},"alternative-id":["252"],"URL":"https:\/\/doi.org\/10.1007\/s10703-016-0252-9","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2016,4]]}}}