{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,10,4]],"date-time":"2023-10-04T15:09:59Z","timestamp":1696432199469},"reference-count":53,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2016,3,23]],"date-time":"2016-03-23T00:00:00Z","timestamp":1458691200000},"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":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2017,8]]},"DOI":"10.1007\/s10009-016-0418-1","type":"journal-article","created":{"date-parts":[[2016,3,23]],"date-time":"2016-03-23T07:56:33Z","timestamp":1458719793000},"page":"449-464","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Synthesizing, correcting and improving code, using model checking-based genetic programming"],"prefix":"10.1007","volume":"19","author":[{"given":"Gal","family":"Katz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Doron","family":"Peled","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,3,23]]},"reference":[{"issue":"6","key":"418_CR1","doi-asserted-by":"crossref","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"22","author":"KR Apt","year":"1986","unstructured":"Apt, K.R., Kozen, D.C.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 22(6), 307\u2013309 (1986)","journal-title":"Inf. Process. Lett."},{"key":"418_CR2","unstructured":"Banzhaf, W., Nordin, P., Keller, R.E., Francone, F.D.: Genetic Programming\u2014An Introduction; On the Automatic Evolution of Computer Programs and its Applications. 3rd edn. Morgan Kaufmann, dpunkt.verlag (2001)"},{"key":"418_CR3","doi-asserted-by":"crossref","unstructured":"Bar-David, Y., Taubenfeld, G.: Automatic discovery of mutual exclusion algorithms. In: PODC, p. 305 (2003)","DOI":"10.1145\/872035.872080"},{"issue":"4","key":"418_CR4","doi-asserted-by":"crossref","first-page":"387","DOI":"10.1162\/evco.1998.6.4.387","volume":"6","author":"DS Burke","year":"1998","unstructured":"Burke, D.S., Jong, K.A.D., Grefenstette, J.J., Ramsey, C.L., Wu, A.S.: Putting more genetics into genetic algorithms. Evolut. Comput. 6(4), 387\u2013410 (1998)","journal-title":"Evolut. Comput."},{"issue":"2","key":"418_CR5","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1006\/inco.1993.1065","volume":"107","author":"JE Burns","year":"1993","unstructured":"Burns, J.E., Lynch, N.A.: Bounds on shared memory for mutual exclusion. Inform. Comput. 107(2), 171\u2013184 (1993)","journal-title":"Inform. Comput."},{"issue":"5","key":"418_CR6","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1145\/359104.359108","volume":"22","author":"EJH Chang","year":"1979","unstructured":"Chang, E.J.H., Roberts, R.: An improved algorithm for decentralized extrema-finding in circular configurations of processes. Commun. ACM 22(5), 281\u2013283 (1979)","journal-title":"Commun. ACM"},{"issue":"3","key":"418_CR7","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1109\/4235.661552","volume":"1","author":"K Chellapilla","year":"1997","unstructured":"Chellapilla, K.: Evolving computer programs without subtree crossover. IEEE Trans. Evol. Comput. 1(3), 209\u2013216 (1997)","journal-title":"IEEE Trans. Evol. Comput."},{"issue":"5","key":"418_CR8","doi-asserted-by":"crossref","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"EM Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512\u20131542 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"3","key":"418_CR9","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1007\/s100090050035","volume":"2","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Minea, M., Peled, D.: State space reduction using partial order techniques. STTT 2(3), 279\u2013287 (1999)","journal-title":"STTT"},{"key":"418_CR10","volume-title":"Model Checking","author":"EM Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, New York (2000)"},{"issue":"4","key":"418_CR11","doi-asserted-by":"crossref","first-page":"857","DOI":"10.1145\/210332.210339","volume":"42","author":"C Courcoubetis","year":"1995","unstructured":"Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. J. ACM 42(4), 857\u2013907 (1995)","journal-title":"J. ACM"},{"key":"418_CR12","doi-asserted-by":"crossref","unstructured":"Couvreur, J.M., Saheb, N., Sutre, G.: An optimal automata approach to LTL model checking of probabilistic systems. In: LPAR. pp. 361\u2013375 (2003)","DOI":"10.1007\/978-3-540-39813-4_26"},{"issue":"9","key":"418_CR13","doi-asserted-by":"crossref","first-page":"569","DOI":"10.1145\/365559.365617","volume":"8","author":"EW Dijkstra","year":"1965","unstructured":"Dijkstra, E.W.: Solution of a problem in concurrent programming control. Commun. ACM 8(9), 569 (1965)","journal-title":"Commun. ACM"},{"issue":"3","key":"418_CR14","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1016\/0196-6774(82)90023-2","volume":"3","author":"D Dolev","year":"1982","unstructured":"Dolev, D., Klawe, M.M., Rodeh, M.: An o(n log n) unidirectional distributed algorithm for extrema finding in a circle. J. Algorithms 3(3), 245\u2013260 (1982)","journal-title":"J. Algorithms"},{"key":"418_CR15","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Namjoshi, K.S.: Reasoning about rings. In: POPL, pp. 85\u201394 (1995)","DOI":"10.1145\/199448.199468"},{"key":"418_CR16","doi-asserted-by":"crossref","unstructured":"Fearnley, J., Peled, D., Schewe, S.: Synthesis of succinct systems. In: ATVA, pp. 208\u2013222 (2012)","DOI":"10.1007\/978-3-642-33386-6_18"},{"key":"418_CR17","doi-asserted-by":"crossref","unstructured":"Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Protocol Specification, Testing and Verification XV, Proceedings of the Fifteenth IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification, Warsaw, Poland, pp. 3\u201318 (1995)","DOI":"10.1007\/978-0-387-34892-6_1"},{"issue":"14","key":"418_CR18","doi-asserted-by":"crossref","first-page":"905","DOI":"10.1016\/S0950-5849(01)00196-3","volume":"43","author":"M Harman","year":"2001","unstructured":"Harman, M., Jones, B.F.: Software engineering using metaheuristic innovative algorithms: workshop report. Inform. Softw. Technol. 43(14), 905\u2013907 (2001)","journal-title":"Inform. Softw. Technol."},{"key":"418_CR19","doi-asserted-by":"crossref","unstructured":"Hinton, A., Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM: a tool for automatic verification of probabilistic systems. In Tools and Algorithms for the Construction and Analysis of Systems TACAS 2006, 441\u2013444 (2006)","DOI":"10.1007\/11691372_29"},{"issue":"10","key":"418_CR20","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"418_CR21","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/1090.001.0001","volume-title":"Adaptation in Natural and Artificial Systems: An Introductory Analysis with Applications to Biology, Control and Artificial Intelligence","author":"JH Holland","year":"1992","unstructured":"Holland, J.H.: Adaptation in Natural and Artificial Systems: An Introductory Analysis with Applications to Biology, Control and Artificial Intelligence. MIT Press, Cambridge (1992)"},{"key":"418_CR22","doi-asserted-by":"crossref","unstructured":"Johnson, C.G.: Genetic programming with fitness based on model checking. In: Genetic Programming, 10th European Conference, EuroGP 2007, Valencia, Spain, April 11\u201313, 2007, Proceedings, pp.\u00a0114\u2013124 (2007)","DOI":"10.1007\/978-3-540-71605-1_11"},{"key":"418_CR23","doi-asserted-by":"crossref","unstructured":"Katz, G., Peled, D.: Genetic programming and model checking: synthesizing new mutual exclusion algorithms. In: ATVA, vol.\u00a05311 of LNCS, pp.\u00a033\u201347 (2008)","DOI":"10.1007\/978-3-540-88387-6_5"},{"key":"418_CR24","doi-asserted-by":"crossref","unstructured":"Katz, G., Peled, D.: Model checking-based genetic programming with an application to mutual exclusion. In: TACAS, vol.\u00a04963 of LNCS, pp.\u00a0141\u2013156 (2008)","DOI":"10.1007\/978-3-540-78800-3_11"},{"key":"418_CR25","doi-asserted-by":"crossref","unstructured":"Katz, G., Peled, D.: Synthesizing solutions to the leader election problem using model checking and genetic programming. In: HVC, vol.\u00a06405 of LNCS, pp.\u00a0117\u2013132 (2009)","DOI":"10.1007\/978-3-642-19237-1_13"},{"key":"418_CR26","unstructured":"Katz, G., Peled, D.: Synthesizing solutions to the leader election problem using model checking and genetic programming. In: HVC (2009)"},{"key":"418_CR27","doi-asserted-by":"crossref","unstructured":"Katz, G., Peled, D.: Code mutation in verification and automatic code correction. In: TACAS, pp.\u00a0435\u2013450 (2010)","DOI":"10.1007\/978-3-642-12002-2_36"},{"key":"418_CR28","doi-asserted-by":"crossref","unstructured":"Katz, G., Peled, D.: Mcgp: a software synthesis tool based on model checking and genetic programming. In: ATVA, pp.\u00a0359\u2013364 (2010)","DOI":"10.1007\/978-3-642-15643-4_28"},{"key":"418_CR29","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/BF00288966","volume":"17","author":"JLW Kessels","year":"1982","unstructured":"Kessels, J.L.W.: Arbitration without common modifiable variables. Acta Inf. 17, 135\u2013141 (1982)","journal-title":"Acta Inf."},{"key":"418_CR30","volume-title":"Genetic Programming: On the Programming of Computers by Means of Natural Selection","author":"JR Koza","year":"1992","unstructured":"Koza, J.R.: Genetic Programming: On the Programming of Computers by Means of Natural Selection. MIT Press, Cambridge (1992)"},{"issue":"3\u20134","key":"418_CR31","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1007\/s10710-010-9112-3","volume":"11","author":"JR Koza","year":"2010","unstructured":"Koza, J.R.: Human-competitive results produced by genetic programming. Genet. Program. Evol. Mach. 11(3\u20134), 251\u2013284 (2010)","journal-title":"Genet. Program. Evol. Mach."},{"issue":"3","key":"418_CR32","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal Methods Syst. Design 19(3), 291\u2013314 (2001)","journal-title":"Formal Methods Syst. Design"},{"key":"418_CR33","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.Y.: Synthesizing distributed systems. In: 16th Annual IEEE Symposium on Logic in Computer Science, Boston, Massachusetts, USA, June 16\u201319, 2001, Proceedings, pp.\u00a0389\u2013398 (2001)","DOI":"10.1109\/LICS.2001.932514"},{"issue":"1","key":"418_CR34","doi-asserted-by":"crossref","first-page":"118","DOI":"10.1109\/TEVC.2013.2281544","volume":"19","author":"WB Langdon","year":"2015","unstructured":"Langdon, W.B., Harman, M.: Optimizing existing software with genetic programming. IEEE Trans. Evol. Comput. 19(1), 118\u2013135 (2015)","journal-title":"IEEE Trans. Evol. Comput."},{"key":"418_CR35","doi-asserted-by":"crossref","unstructured":"Lehmann, D.J., Pnueli, A., Stavi, J.: Impartiality, justice and fairness: The ethics of concurrent termination. In: Automata, Languages and Programming, 8th Colloquium, Acre (Akko), Israel, Proceedings, pp.\u00a0264\u2013277 (1981)","DOI":"10.1007\/3-540-10843-2_22"},{"key":"418_CR36","doi-asserted-by":"crossref","unstructured":"Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages, New Orleans, Louisiana, USA, pp.\u00a097\u2013107 (1985)","DOI":"10.1145\/318593.318622"},{"key":"418_CR37","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: How to cook a temporal proof system for your pet language. In: Conference Record of the Tenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, January 1983, pp.\u00a0141\u2013154 (1983)","DOI":"10.1145\/567067.567082"},{"issue":"1","key":"418_CR38","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1145\/357233.357237","volume":"6","author":"Z Manna","year":"1984","unstructured":"Manna, Z., Wolper, P.: Synthesis of communicating processes from temporal logic specifications. ACM Trans. Program. Lang. Syst. 6(1), 68\u201393 (1984)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"418_CR39","doi-asserted-by":"crossref","unstructured":"Montana, D.J.: Strongly typed genetic programming. Evol. Comput. 3(2), 199\u2013230 (1995)","DOI":"10.1162\/evco.1995.3.2.199"},{"key":"418_CR40","doi-asserted-by":"crossref","unstructured":"Niebert, P., Peled, D., Pnueli, A.: Discriminative model checking. In: CAV, vol.\u00a05123 of LNCS, Springer, pp.\u00a0504\u2013516 (2008)","DOI":"10.1007\/978-3-540-70545-1_48"},{"issue":"12","key":"418_CR41","doi-asserted-by":"crossref","first-page":"1173","DOI":"10.1002\/cpe.903","volume":"16","author":"JA Perez","year":"2004","unstructured":"Perez, J.A., Corchuelo, R., Toro, M.: An order-based algorithm for implementing multiparty synchronization. Concurr. Pract. Exp. 16(12), 1173\u20131206 (2004)","journal-title":"Concurr. Pract. Exp."},{"key":"418_CR42","doi-asserted-by":"crossref","unstructured":"Peterson, F.: Economical solutions to the critical section problem in a distributed system. In: STOC: ACM Symposium on Theory of Computing (STOC) (1977)","DOI":"10.1145\/800105.803398"},{"issue":"4","key":"418_CR43","doi-asserted-by":"crossref","first-page":"758","DOI":"10.1145\/69622.357194","volume":"4","author":"GL Peterson","year":"1982","unstructured":"Peterson, G.L.: An o(n log n) unidirectional algorithm for the circular extrema problem. ACM Trans. Program. Lang. Syst. 4(4), 758\u2013762 (1982)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"418_CR44","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL, pp.\u00a0179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"key":"418_CR45","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: Distributed reactive systems are hard to synthesize. In: FOCS, pp.\u00a0746\u2013757 (1990)","DOI":"10.1109\/FSCS.1990.89597"},{"key":"418_CR46","unstructured":"Poli, R., Langdon, W.W.B., McPhee, N.F., Koza, J.R.: A field guide to genetic programming. Lulu. com (2008)"},{"key":"418_CR47","doi-asserted-by":"crossref","unstructured":"Safra, S.: On the complexity of omega-automata. In: 29th Annual Symposium on Foundations of Computer Science, White Plains, New York, USA, 24\u201326 October 1988, pp.\u00a0319\u2013327 (1988)","DOI":"10.1109\/SFCS.1988.21948"},{"key":"418_CR48","volume-title":"Evolution and Optimum Seeking: The Sixth Generation","author":"H-PP Schwefel","year":"1993","unstructured":"Schwefel, H.-P.P.: Evolution and Optimum Seeking: The Sixth Generation. Wiley, New York (1993)"},{"key":"418_CR49","doi-asserted-by":"crossref","unstructured":"Thomas, W.: Automata on infinite objects. In: Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), pp.\u00a0133\u2013192 (1990)","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"418_CR50","doi-asserted-by":"crossref","unstructured":"Tsay, Y.K.: Deriving a scalable algorithm for mutual exclusion. In: DISC, pp.\u00a0393\u2013407 (1998)","DOI":"10.1007\/BFb0056497"},{"key":"418_CR51","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: Probabilistic linear-time model checking: An overview of the automata-theoretic approach. In: Formal Methods for Real-Time and Probabilistic Systems, 5th International AMAST Workshop, ARTS\u201999, Bamberg, Germany, pp.\u00a0265\u2013276 (1999)","DOI":"10.1007\/3-540-48778-6_16"},{"key":"418_CR52","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proceedings of IEEE Symposium on Logic in Computer Science, Boston. pp.\u00a0332\u2013344 (1986)"},{"issue":"3\u20134","key":"418_CR53","first-page":"139","volume":"30","author":"LD Zuck","year":"2004","unstructured":"Zuck, L.D., Pnueli, A.: Model checking and abstraction to the aid of parameterized systems (a survey). Comp. Lang. Syst. Struct. 30(3\u20134), 139\u2013169 (2004)","journal-title":"Comp. Lang. Syst. Struct."}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-016-0418-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-016-0418-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-016-0418-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-016-0418-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,5]],"date-time":"2019-09-05T18:33:51Z","timestamp":1567708431000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-016-0418-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,3,23]]},"references-count":53,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2017,8]]}},"alternative-id":["418"],"URL":"https:\/\/doi.org\/10.1007\/s10009-016-0418-1","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,3,23]]}}}