{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T21:01:07Z","timestamp":1751662867358},"publisher-location":"Berlin, Heidelberg","reference-count":7,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642142949"},{"type":"electronic","value":"9783642142956"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14295-6_38","type":"book-chapter","created":{"date-parts":[[2010,7,8]],"date-time":"2010-07-08T22:36:09Z","timestamp":1278628569000},"page":"430-433","source":"Crossref","is-referenced-by-count":7,"title":["Comfusy: A Tool for Complete Functional Synthesis"],"prefix":"10.1007","author":[{"given":"Viktor","family":"Kuncak","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mika\u00ebl","family":"Mayer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ruzica","family":"Piskac","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Philippe","family":"Suter","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"38_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-540-73368-3_29","volume-title":"Computer Aided Verification","author":"B. Jobstmann","year":"2007","unstructured":"Jobstmann, B., Galler, S., Weiglhofer, M., Bloem, R.: Anzu: A tool for property synthesis. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 258\u2013262. Springer, Heidelberg (2007)"},{"key":"38_CR2","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Complete functional synthesis. In: ACM Conf. Programming Language Design and Implementation, PLDI (2010)","DOI":"10.1145\/1806596.1806632"},{"issue":"3","key":"38_CR3","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/s10817-006-9042-1","volume":"36","author":"V. Kuncak","year":"2006","unstructured":"Kuncak, V., Nguyen, H.H., Rinard, M.: Deciding Boolean Algebra with Presburger Arithmetic. Journal of Automated Reasoning\u00a036(3), 213\u2013239 (2006)","journal-title":"Journal of Automated Reasoning"},{"issue":"3","key":"38_CR4","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/362566.362568","volume":"14","author":"Z. Manna","year":"1971","unstructured":"Manna, Z., Waldinger, R.J.: Toward automatic program synthesis. Communications of the ACM\u00a014(3), 151\u2013165 (1971)","journal-title":"Communications of the ACM"},{"key":"38_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"38_CR6","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: ACM Symp. Principles of Programming Languages, POPL (1989)","DOI":"10.1145\/75277.75293"},{"issue":"8","key":"38_CR7","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1145\/135226.135233","volume":"35","author":"W. Pugh","year":"1992","unstructured":"Pugh, W.: A practical algorithm for exact array dependence analysis. Communications of the ACM\u00a035(8), 102\u2013114 (1992)","journal-title":"Communications of the ACM"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14295-6_38.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T12:23:36Z","timestamp":1619785416000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14295-6_38"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642142949","9783642142956"],"references-count":7,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14295-6_38","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}