{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T03:47:25Z","timestamp":1725594445099},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642223051"},{"type":"electronic","value":"9783642223068"}],"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-22306-8_9","type":"book-chapter","created":{"date-parts":[[2011,7,4]],"date-time":"2011-07-04T07:25:05Z","timestamp":1309764305000},"page":"126-143","source":"Crossref","is-referenced-by-count":3,"title":["Program Sketching via CTL* Model Checking"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Morgenstern","sequence":"first","affiliation":[]},{"given":"Klaus","family":"Schneider","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"9_CR1","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1109\/JPROC.2002.805826","volume":"91","author":"A. Benveniste","year":"2003","unstructured":"Benveniste, A., Caspi, P., Edwards, S., Halbwachs, N., Le Guernic, P., de Simone, R.: The synchronous languages twelve years later. Proceedings of the IEEE\u00a091(1), 64\u201383 (2003)","journal-title":"Proceedings of the IEEE"},{"key":"9_CR2","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2007.09.004","volume":"190","author":"R. Bloem","year":"2007","unstructured":"Bloem, R., Galler, S., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Specify, compile, run: Hardware from PSL. Electronic Notes in Theoretical Computer Science (ENTCS)\u00a0190, 3\u201316 (2007)","journal-title":"Electronic Notes in Theoretical Computer Science (ENTCS)"},{"key":"9_CR3","first-page":"339","volume-title":"Principles of Programming Languages (POPL)","author":"R. Bod\u00edk","year":"2010","unstructured":"Bod\u00edk, R., Chandra, S., Galenson, J., Kimelman, D., Tung, N., Barman, S., Rodarmor, C.: Programming with angelic nondeterminism. In: Hermenegildo, M., Palsberg, J. (eds.) Principles of Programming Languages (POPL), Madrid, Spain, pp. 339\u2013352. ACM, New York (2010)"},{"key":"9_CR4","volume-title":"A Discipline of Programming","author":"E. Dijkstra","year":"1976","unstructured":"Dijkstra, E.: A Discipline of Programming. Prentice Hall, Englewood Cliffs (1976)"},{"key":"9_CR5","first-page":"995","volume-title":"Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics","author":"E.A. Emerson","year":"1990","unstructured":"Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, ch.16, pp. 995\u20131072. Elsevier, Amsterdam (1990)"},{"key":"9_CR6","first-page":"84","volume-title":"Principles of Programming Languages (POPL)","author":"E.A. Emerson","year":"1985","unstructured":"Emerson, E.A., Lei, C.-L.: Modalities for model checking: Branching time strikes back. In: Principles of Programming Languages (POPL), pp. 84\u201396. ACM, USA (1985)"},{"key":"9_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-642-15643-4_10","volume-title":"Automated Technology for Verification and Analysis","author":"E. Filiot","year":"2010","unstructured":"Filiot, E., Jin, N., Raskin, J.-F.: Compositional algorithms for LTL synthesis. In: Bouajjani, A., Chin, W.-N. (eds.) ATVA 2010. LNCS, vol.\u00a06252, pp. 112\u2013127. Springer, Heidelberg (2010)"},{"key":"9_CR8","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-2231-4","volume-title":"Synchronous programming of reactive systems","author":"N. Halbwachs","year":"1993","unstructured":"Halbwachs, N.: Synchronous programming of reactive systems. Kluwer, Dordrecht (1993)"},{"key":"9_CR9","volume-title":"The Art of Computer Programming","author":"D. Knuth","year":"1998","unstructured":"Knuth, D.: The Art of Computer Programming, vol.\u00a02. Addison-Wesley, London (1998)"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Morgenstern, A., Schneider, K.: A LTL fragment for GR(1)-synthesis. In: International Workshop on Interactions, Games and Protocols (IWIGP), Electronic Proceedings in Theoretical Computer Science (EPTCS), Saarbr\u00fccken, Germany (2011)","DOI":"10.4204\/EPTCS.50.3"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"474","DOI":"10.1007\/978-3-540-75596-8_33","volume-title":"Automated Technology for Verification and Analysis","author":"S. Schewe","year":"2007","unstructured":"Schewe, S., Finkbeiner, B.: Bounded synthesis. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol.\u00a04762, pp. 474\u2013488. Springer, Heidelberg (2007)"},{"key":"9_CR12","volume-title":"Texts in Theoretical Computer Science (EATCS Series)","author":"K. Schneider","year":"2003","unstructured":"Schneider, K.: Verification of Reactive Systems - Formal Methods and Algorithms. In: Texts in Theoretical Computer Science (EATCS Series). Springer, Heidelburg (2003)"},{"key":"9_CR13","unstructured":"Schneider, K.: The synchronous programming language Quartz. Internal Report 375, Department of Computer Science, University of Kaiserslautern, Kaiserslautern (2009)"},{"issue":"5","key":"9_CR14","first-page":"175","volume":"24","author":"E. Shade","year":"2009","unstructured":"Shade, E.: Size matters: lessons from a broken binary search. Journal of Computing Sciences in Colleges (JCSC)\u00a024(5), 175\u2013182 (2009)","journal-title":"Journal of Computing Sciences in Colleges (JCSC)"},{"key":"9_CR15","unstructured":"Solar-Lezama, A.: Program Synthesis by Sketching. PhD thesis, University of California, Berkeley, California, USA (2008)"},{"key":"9_CR16","first-page":"281","volume-title":"Programming Language Design and Implementation (PLDI)","author":"A. Solar-Lezama","year":"2005","unstructured":"Solar-Lezama, A., Rabbah, R.,Bod\u00edk, R., Ebcio\u011flu, K.: Programming by sketching for bit streaming programs. In: Hall, M. (ed.) Programming Language Design and Implementation (PLDI), pp. 281\u2013294. ACM, Chicago (2005)"},{"key":"9_CR17","first-page":"404","volume-title":"Architectural Support for Programming Languages and Operating Systems (ASPLOS)","author":"A. Solar-Lezama","year":"2006","unstructured":"Solar-Lezama, A., Tancau, L., Bodik, R., Saraswat, V., Seshia, S.: Combinatorial sketching for finite programs. In: Architectural Support for Programming Languages and Operating Systems (ASPLOS), pp. 404\u2013415. ACM, USA (2006)"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22306-8_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,12]],"date-time":"2019-06-12T13:34:31Z","timestamp":1560346471000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22306-8_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642223051","9783642223068"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22306-8_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}