{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T05:06:27Z","timestamp":1725858387029},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319415901"},{"type":"electronic","value":"9783319415918"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-41591-8_11","type":"book-chapter","created":{"date-parts":[[2016,6,23]],"date-time":"2016-06-23T17:27:27Z","timestamp":1466702847000},"page":"155-171","source":"Crossref","is-referenced-by-count":1,"title":["Program Generation Using Simulated Annealing and Model Checking"],"prefix":"10.1007","author":[{"given":"Idress","family":"Husien","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sven","family":"Schewe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,6,23]]},"reference":[{"key":"11_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"521","DOI":"10.1007\/BFb0028774","volume-title":"Computer Aided Verification","author":"R Alur","year":"1998","unstructured":"Alur, R., Henzinger, T.A., Mang, F.Y.C., Qadeer, S., Rajamani, S.K., Tasiran, S.: MOCHA: modularity in model checking. In: Hu, A.L., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 521\u2013525. Springer, Heidelberg (1998)"},{"issue":"2","key":"11_CR2","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"JR Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: $$10^{20}$$ states and beyond. Inf. Comput. 98(2), 142\u2013170 (1992)","journal-title":"Inf. Comput."},{"key":"11_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359\u2013364. Springer, Heidelberg (2002)"},{"key":"11_CR4","doi-asserted-by":"crossref","first-page":"891","DOI":"10.1016\/S0950-5849(01)00195-1","volume":"43","author":"JA Clark","year":"2001","unstructured":"Clark, J.A., Jacob, J.L.: Protocols are programs too: the meta-heuristic search for security protocols. Inf. Softw. Technol. 43, 891\u2013904 (2001)","journal-title":"Inf. Softw. Technol."},{"key":"11_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"EM Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logics of Programs. LNCS, vol. 131, pp. 52\u201371. Springer, Heidelberg (1982)"},{"key":"11_CR6","volume-title":"Model Checking","author":"EM Clarke Jr","year":"1999","unstructured":"Clarke Jr., E.M., Grumberg, O., Peled, O.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/978-3-662-48899-7_34","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C David","year":"2015","unstructured":"David, C., Kroening, D., Lewis, M.: Using program synthesis for program analysis. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR-20 2015. LNCS, vol. 9450, pp. 483\u2013498. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-48899-7_34"},{"key":"11_CR8","volume-title":"Genetic Algorithms and Simulated Annealing","author":"L Davis","year":"1987","unstructured":"Davis, L.: Genetic Algorithms and Simulated Annealing. Morgan Kaufmann Publishers Inc., San Francisco (1987)"},{"key":"11_CR9","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, 569 (1965)","journal-title":"Commun. ACM"},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"272","DOI":"10.1007\/978-3-642-19835-9_25","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Ehlers","year":"2011","unstructured":"Ehlers, R.: Unbeast: symbolic bounded synthesis. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 272\u2013275. Springer, Heidelberg (2011)"},{"issue":"7","key":"11_CR11","doi-asserted-by":"crossref","first-page":"1171","DOI":"10.1016\/j.jcss.2015.02.005","volume":"81","author":"J Fearnley","year":"2015","unstructured":"Fearnley, J., Peled, D., Schewe, S.: Synthesis of succinct systems. J. Comput. Syst. Sci. 81(7), 1171\u20131193 (2015)","journal-title":"J. Comput. Syst. Sci."},{"key":"11_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1007\/978-3-642-02658-4_22","volume-title":"Computer Aided Verification","author":"E Filiot","year":"2009","unstructured":"Filiot, E., Jin, N., Raskin, J.-F.: An antichain algorithm for LTL realizability. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 263\u2013277. Springer, Heidelberg (2009)"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"Finkbeiner, B., Schewe, S.: Uniform distributed synthesis. In: LICS, pp. 321\u2013330. IEEE Computer Society Press (2005)","DOI":"10.1109\/LICS.2005.53"},{"issue":"5\u20136","key":"11_CR14","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.: Bounded synthesis. Int. J. Softw. Tools Technol. Transfer 15(5\u20136), 519\u2013539 (2013)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"312","DOI":"10.1007\/978-3-319-06410-9_22","volume-title":"FM 2014: Formal Methods","author":"EM Hahn","year":"2014","unstructured":"Hahn, E.M., Li, Y., Schewe, S., Turrini, A., Zhang, L.: iscasMc: a web-based probabilistic model checker. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 312\u2013317. Springer, Heidelberg (2014)"},{"key":"11_CR16","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/0-306-48056-5_10","volume-title":"Handbook of Metaheuristics","author":"D Henderson","year":"2003","unstructured":"Henderson, D., Jacobson, S.H., Johnson, A.W.: The theory and practice of simulated annealing. In: Glover, F., Kochenberger, G.A. (eds.) Handbook of Metaheuristics, pp. 287\u2013319. Springer, New York (2003)"},{"key":"11_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1007\/978-3-642-40184-8_20","volume-title":"CONCUR 2013 \u2013 Concurrency Theory","author":"TA Henzinger","year":"2013","unstructured":"Henzinger, T.A., Otop, J.: From model checking to model measuring. In: D\u2019Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013 \u2013 Concurrency Theory. LNCS, vol. 8052, pp. 273\u2013287. Springer, Heidelberg (2013)"},{"issue":"5","key":"11_CR18","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"GJ Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. Softw. Eng. 23(5), 279\u2013295 (1997)","journal-title":"Softw. Eng."},{"key":"11_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"226","DOI":"10.1007\/11513988_23","volume-title":"Computer Aided Verification","author":"B Jobstmann","year":"2005","unstructured":"Jobstmann, B., Griesmayer, A., Bloem, R.: Program repair as a game. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 226\u2013238. Springer, Heidelberg (2005)"},{"key":"11_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"114","DOI":"10.1007\/978-3-540-71605-1_11","volume-title":"Genetic Programming","author":"CG 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. 4445, pp. 114\u2013124. Springer, Heidelberg (2007)"},{"key":"11_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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.A.: Model checking-based genetic programming with an application to mutual exclusion. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 141\u2013156. Springer, Heidelberg (2008)"},{"key":"11_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. 5348, pp. 122\u2013131. Springer, Heidelberg (2009)"},{"key":"11_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1007\/978-3-642-19237-1_13","volume-title":"Hardware and Software: Verification and Testing","author":"G Katz","year":"2011","unstructured":"Katz, G., Peled, D.: Synthesizing solutions to the leader election problem using model checking and genetic programming. In: Namjoshi, K., Zeller, A., Ziv, A. (eds.) HVC 2009. LNCS, vol. 6405, pp. 117\u2013132. Springer, Heidelberg (2011)"},{"key":"11_CR24","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":"2","key":"11_CR25","doi-asserted-by":"crossref","first-page":"245","DOI":"10.2307\/421091","volume":"5","author":"O Kupferman","year":"1999","unstructured":"Kupferman, O., Vardi, M.Y.: Church\u2019s problem revisited. Bull. Symb. Logic 5(2), 245\u2013263 (1999)","journal-title":"Bull. Symb. Logic"},{"issue":"2","key":"11_CR26","doi-asserted-by":"crossref","first-page":"312","DOI":"10.1145\/333979.333987","volume":"47","author":"O Kupferman","year":"2000","unstructured":"Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. J. ACM 47(2), 312\u2013360 (2000)","journal-title":"J. ACM"},{"key":"11_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011)"},{"key":"11_CR28","unstructured":"Lahtinen, J., Myllym\u00e4ki, P., Silander, T., Tirri, H.: Empirical comparison of stochastic algorithms. In: 2NWGA, pp. 45\u201360 (1996)"},{"key":"11_CR29","doi-asserted-by":"crossref","unstructured":"Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: POPL, pp. 97\u2013107. ACM (1985)","DOI":"10.1145\/318593.318622"},{"key":"11_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"396","DOI":"10.1007\/3-540-48224-5_33","volume-title":"Automata, Languages and Programming","author":"P Madhusudan","year":"2001","unstructured":"Madhusudan, P., Thiagarajan, P.S.: Distributed controller synthesis for local specifications. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 396\u2013407. Springer, Heidelberg (2001)"},{"key":"11_CR31","unstructured":"Mann, J., Smith, G.: A comparison of heuristics for telecommunications traffic routing. In: Modern Heuristic Search Methods, pp. 235\u2013254 (1996)"},{"key":"11_CR32","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46\u201357. IEEE Computer Society Press (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"11_CR33","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: Distributed reactive systems are hard to synthesize. In: FOCS, pp. 746\u2013757. IEEE Computer Society Press (1990)","DOI":"10.1109\/FSCS.1990.89597"},{"key":"11_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1007\/978-3-540-71410-1_10","volume-title":"Logic-Based Program Synthesis and Transformation","author":"S Schewe","year":"2007","unstructured":"Schewe, S., Finkbeiner, B.: Synthesis of asynchronous systems. In: Puebla, G. (ed.) LOPSTR 2006. LNCS, vol. 4407, pp. 127\u2013142. Springer, Heidelberg (2007)"},{"issue":"5\u20136","key":"11_CR35","doi-asserted-by":"crossref","first-page":"475","DOI":"10.1007\/s10009-012-0249-7","volume":"15","author":"A Solar-Lezama","year":"2013","unstructured":"Solar-Lezama, A.: Program sketching. Int. J. Softw. Tools Technol. Transf. 15(5\u20136), 475\u2013495 (2013)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"11_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"896","DOI":"10.1007\/978-3-642-39799-8_64","volume-title":"Computer Aided Verification","author":"C Essen von","year":"2013","unstructured":"von Essen, C., Jobstmann, B.: Program repair without regret. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 896\u2013911. Springer, Heidelberg (2013)"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-41591-8_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T16:57:26Z","timestamp":1498323446000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-41591-8_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319415901","9783319415918"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-41591-8_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}