{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,29]],"date-time":"2025-11-29T07:48:06Z","timestamp":1764402486516,"version":"3.38.0"},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642192364"},{"type":"electronic","value":"9783642192371"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-19237-1_13","type":"book-chapter","created":{"date-parts":[[2011,2,10]],"date-time":"2011-02-10T07:15:37Z","timestamp":1297322137000},"page":"117-132","source":"Crossref","is-referenced-by-count":13,"title":["Synthesizing Solutions to the Leader Election Problem Using Model Checking and Genetic Programming"],"prefix":"10.1007","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","reference":[{"issue":"6","key":"13_CR1","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"22","author":"K.R. Apt","year":"1986","unstructured":"Apt, K.R., Kozen, D.C.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett.\u00a022(6), 307\u2013309 (1986)","journal-title":"Inf. Process. Lett."},{"key":"13_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/978-3-540-39989-6_10","volume-title":"Distributed Computing","author":"Y. Bar-David","year":"2003","unstructured":"Bar-David, Y., Taubenfeld, G.: Automatic discovery of mutual exclusion algorithms. In: Fich, F.E. (ed.) DISC 2003. LNCS, vol.\u00a02848, pp. 136\u2013150. Springer, Heidelberg (2003)"},{"issue":"5","key":"13_CR3","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1145\/359104.359108","volume":"22","author":"E. Chang","year":"1979","unstructured":"Chang, E., Roberts, R.: An improved algorithm for decentralized extrema-finding in circular configurations of processes. ACM Commun.\u00a022(5), 281\u2013283 (1979)","journal-title":"ACM Commun."},{"issue":"3","key":"13_CR4","doi-asserted-by":"publisher","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. Evolutionary Computation\u00a01(3), 209\u2013216 (1997)","journal-title":"IEEE Trans. Evolutionary Computation"},{"issue":"3","key":"13_CR5","doi-asserted-by":"publisher","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 logn ) unidirectional distributed algorithm for extrema finding in a circle. J. Algorithms\u00a03(3), 245\u2013260 (1982)","journal-title":"J. Algorithms"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/978-3-540-30124-0_26","volume-title":"Computer Science Logic","author":"E.A. Emerson","year":"2004","unstructured":"Emerson, E.A., Kahlon, V.: Parameterized model checking of ring-based message passing systems. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol.\u00a03210, pp. 325\u2013339. Springer, Heidelberg (2004)"},{"issue":"4","key":"13_CR7","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1142\/S0129054103001881","volume":"14","author":"E.A. Emerson","year":"2003","unstructured":"Emerson, E.A., Namjoshi, K.S.: On reasoning about rings. Int. J. Found. Comput. Sci.\u00a014(4), 527\u2013550 (2003)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"13_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"438","DOI":"10.1007\/3-540-56922-7_36","volume-title":"Computer Aided Verification","author":"P. Godefroid","year":"1993","unstructured":"Godefroid, P., Pirottin, D.: Refining dependencies improves partial-order verification methods (extended abstract). In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, pp. 438\u2013449. Springer, Heidelberg (1993)"},{"key":"13_CR9","first-page":"23","volume-title":"The Spin Verification System","author":"G. Holzmann","year":"1996","unstructured":"Holzmann, G., Peled, D., Yannakakis, M.: On nested depth first search. In: The Spin Verification System, pp. 23\u201332. American Mathematical Society, Providence (1996)"},{"key":"13_CR10","volume-title":"The SPIN Model Checker","author":"G.J. Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The SPIN Model Checker. Pearson Education, London (2003)"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J., Peled, D.: An improvement in formal verification. In: FORTE, pp. 197\u2013211 (1994)","DOI":"10.1007\/978-0-387-34878-0_13"},{"key":"13_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-540-71605-1_11","volume-title":"Genetic Programming","author":"C.G. Johnson","year":"2007","unstructured":"Johnson, C.G.: Genetic programming with fitness based on model checking. In: Ebner, M., O\u2019Neill, M., Ek\u00e1rt, A., Vanneschi, L., Esparcia-Alc\u00e1zar, A.I. (eds.) EuroGP 2007. LNCS, vol.\u00a04445, pp. 114\u2013124. Springer, Heidelberg (2007)"},{"key":"13_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-540-88387-6_5","volume-title":"Automated Technology for Verification and Analysis","author":"G. Katz","year":"2008","unstructured":"Katz, G., Peled, D.: Genetic programming and model checking: Synthesizing new mutual exclusion algorithms. In: Cha, S(S.), Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol.\u00a05311, pp. 33\u201347. Springer, Heidelberg (2008)"},{"key":"13_CR14","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.: Model checking-based genetic programming with an application to mutual exclusion. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 141\u2013156. Springer, Heidelberg (2008)"},{"key":"13_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-642-00431-5_8","volume-title":"Model Checking and Artificial Intelligence","author":"G. Katz","year":"2009","unstructured":"Katz, G., Peled, D.: Model checking driven heuristic search for correct programs. In: Peled, D.A., Wooldridge, M.J. (eds.) MoChArt 2008. LNCS, vol.\u00a05348, pp. 122\u2013131. Springer, Heidelberg (2009)"},{"issue":"2","key":"13_CR16","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1016\/0304-3975(92)90054-J","volume":"101","author":"S. Katz","year":"1992","unstructured":"Katz, S., Peled, D.: Defining conditional independence using collapses. Theor. Comput. Sci.\u00a0101(2), 337\u2013359 (1992)","journal-title":"Theor. Comput. Sci."},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"Kinnear Jr., K.E.: Evolving a sort: Lessons in genetic programming. In: IJCNN, vol.\u00a02, pp. 881\u2013888 (1993)","DOI":"10.1109\/ICNN.1993.298674"},{"key":"13_CR18","volume-title":"Genetic Programming: On the Programming of Computers by Means of Natural Selection","author":"J.R. Koza","year":"1992","unstructured":"Koza, J.R.: Genetic Programming: On the Programming of Computers by Means of Natural Selection. MIT Press, Cambridge (1992)"},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"Kurshan, R.P., McMillan, K.L.: A structural induction theorem for processes. In: PODC, pp. 239\u2013247 (1989)","DOI":"10.1145\/72981.72998"},{"key":"13_CR20","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/BF01786631","volume":"4","author":"L. Lamport","year":"1990","unstructured":"Lamport, L.: A theorem on atomicity in distributed algorithms. Distributed Computing\u00a04, 59\u201368 (1990)","journal-title":"Distributed Computing"},{"key":"13_CR21","unstructured":"Le Lann, G.: Distributed systems - towards a formal approach. In: IFIP Congress, pp. 155\u2013160 (1977)"},{"key":"13_CR22","doi-asserted-by":"crossref","unstructured":"Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: POPL, pp. 97\u2013107 (1985)","DOI":"10.1145\/318593.318622"},{"key":"13_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1007\/978-3-540-70545-1_48","volume-title":"Computer Aided Verification","author":"P. Niebert","year":"2008","unstructured":"Niebert, P., Peled, D., Pnueli, A.: Discriminative model checking. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 504\u2013516. Springer, Heidelberg (2008)"},{"issue":"3","key":"13_CR24","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1016\/0022-0000(78)90021-1","volume":"16","author":"D.C. Oppen","year":"1978","unstructured":"Oppen, D.C.: A $2^{2^{2^{pn}}}$ upper bound on the complexity of presburger arithmetic. J. Comput. Syst. Sci.\u00a016(3), 323\u2013332 (1978)","journal-title":"J. Comput. Syst. Sci."},{"key":"13_CR25","unstructured":"Overman, W.T., Crocker, S.D.: Verification of concurrent systems: Function and timing. In: PSTV, pp. 401\u2013409 (1982)"},{"issue":"4","key":"13_CR26","doi-asserted-by":"publisher","first-page":"758","DOI":"10.1145\/69622.357194","volume":"4","author":"G.L. Peterson","year":"1982","unstructured":"Peterson, G.L.: An O(n log n) unidirectional algorithm for the circular extrema problem. ACM Trans. Program. Lang. Syst.\u00a04(4), 758\u2013762 (1982)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"13_CR27","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"13_CR28","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL, pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"issue":"3","key":"13_CR29","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A.P. Sistla","year":"1985","unstructured":"Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM\u00a032(3), 733\u2013749 (1985)","journal-title":"J. ACM"},{"issue":"4","key":"13_CR30","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1016\/0020-0190(88)90211-6","volume":"28","author":"I. Suzuki","year":"1988","unstructured":"Suzuki, I.: Proving properties of a ring of finite state systems. Inf. Process. Lett.\u00a028(4), 213\u2013314 (1988)","journal-title":"Inf. Process. Lett."},{"key":"13_CR31","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y., Wolper, P.: Automata theoretic techniques for modal logics of programs. In: STOC, pp. 446\u2013456 (1984)","DOI":"10.1145\/800057.808711"},{"key":"13_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/3-540-52148-8_6","volume-title":"Automatic Verification Methods for Finite State Systems","author":"P. Wolper","year":"1990","unstructured":"Wolper, P., Lovinfosse, V.: Verifying properties of large sets of processes with network invariants. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol.\u00a0407, pp. 68\u201380. Springer, Heidelberg (1990)"}],"container-title":["Lecture Notes in Computer Science","Hardware and Software: Verification and Testing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-19237-1_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,2]],"date-time":"2025-03-02T13:44:25Z","timestamp":1740923065000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-19237-1_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642192364","9783642192371"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-19237-1_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}