{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T08:44:40Z","timestamp":1725525880691},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642004308"},{"type":"electronic","value":"9783642004315"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-00431-5_8","type":"book-chapter","created":{"date-parts":[[2009,2,24]],"date-time":"2009-02-24T01:14:35Z","timestamp":1235438075000},"page":"122-131","source":"Crossref","is-referenced-by-count":4,"title":["Model Checking Driven Heuristic Search for Correct Programs"],"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":[{"key":"8_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0035748","volume-title":"Automata, Languages and Programming","author":"M. Abadi","year":"1989","unstructured":"Abadi, M., Lamport, L., Wolper, P.: Realizable and unrealizable specifications of reactive systems. In: Ronchi Della Rocca, S., Ausiello, G., Dezani-Ciancaglini, M. (eds.) ICALP 1989. LNCS, vol.\u00a0372, pp. 1\u201317. Springer, Heidelberg (1989)"},{"key":"8_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)"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/3-540-10003-2_69","volume-title":"Automata, Languages and Programming","author":"E.A. Emerson","year":"1980","unstructured":"Emerson, E.A., Clarke, E.M.: Characterizing correctness properties of parallel programs using fixpoints. In: de Bakker, J.W., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol.\u00a085, pp. 169\u2013181. Springer, Heidelberg (1980)"},{"key":"8_CR4","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":"8_CR5","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":"8_CR6","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/3897.001.0001","volume-title":"An Introduction to Computational Learning Theory","author":"M. Kearns","year":"1994","unstructured":"Kearns, M., Vazirani, U.: An Introduction to Computational Learning Theory. MIT Press, Cambridge (1994)"},{"key":"8_CR7","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":"8_CR8","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":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"International Symposium on Programming","author":"J.P. Quielle","year":"1982","unstructured":"Quielle, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol.\u00a0137, pp. 337\u2013350. Springer, Heidelberg (1982)"},{"key":"8_CR10","doi-asserted-by":"publisher","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 Transactions on Programming Languages and Systems\u00a06, 68\u201393 (1984)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"8_CR11","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)"},{"key":"8_CR12","volume-title":"Heuristics","author":"J. Pearl","year":"1984","unstructured":"Pearl, J.: Heuristics. Addison-Wesley, Reading (1984)"},{"key":"8_CR13","first-page":"46","volume-title":"FOCS 1977","author":"A. Pnueli","year":"1977","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS 1977, Providence, Rhode Island, pp. 46\u201357. IEEE, Los Alamitos (1977)"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of reactive systems. In: POPL 1989, Austin, Texas, pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"key":"8_CR15","volume-title":"FOCS 1990","author":"A. Pnueli","year":"1990","unstructured":"Pnueli, A., Rosner, R.: Distributed Reactive Systems are Hard to Synthesize. In: FOCS 1990, St. Louis, Missouri, vol.\u00a0II. IEEE, Los Alamitos (1990)"},{"key":"8_CR16","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1109\/5.21072","volume":"77","author":"P. Rammage","year":"1989","unstructured":"Rammage, P., Wonham, M.: The control of discrete event systems. Proceedings of the IEEE\u00a077, 81\u201398 (1989)","journal-title":"Proceedings of the IEEE"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/3-540-44585-4_21","volume-title":"Computer Aided Verification","author":"D.X. Song","year":"2001","unstructured":"Song, D.X., Perrig, A., Phan, D.: Agvi \u2013 automatic generation, verification, and implementation of security protocols. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 241\u2013245. Springer, Heidelberg (2001)"},{"issue":"4598","key":"8_CR18","doi-asserted-by":"publisher","first-page":"671","DOI":"10.1126\/science.220.4598.671","volume":"220","author":"S. Kirkpatrick","year":"1983","unstructured":"Kirkpatrick, S., G. Jr., D., Vecchi, M.P.: Optimization by simulated annealing. Science\u00a0220(4598), 671\u2013680 (1983)","journal-title":"Science"},{"key":"8_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1007\/BFb0056497","volume-title":"Distributed Computing","author":"Y.K. Tsay","year":"1998","unstructured":"Tsay, Y.K.: Deriving a scalable algorithm for mutual exclusion. In: Kutten, S. (ed.) DISC 1998. LNCS, vol.\u00a01499, pp. 393\u2013407. Springer, Heidelberg (1998)"}],"container-title":["Lecture Notes in Computer Science","Model Checking and Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-00431-5_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,24]],"date-time":"2023-05-24T00:06:51Z","timestamp":1684886811000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-00431-5_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642004308","9783642004315"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-00431-5_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}