{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T04:18:28Z","timestamp":1745986708897,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642358722"},{"type":"electronic","value":"9783642358739"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-35873-9_8","type":"book-chapter","created":{"date-parts":[[2013,1,2]],"date-time":"2013-01-02T06:22:57Z","timestamp":1357107777000},"page":"88-107","source":"Crossref","is-referenced-by-count":10,"title":["Reductions for Synthesis Procedures"],"prefix":"10.1007","author":[{"given":"Swen","family":"Jacobs","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Viktor","family":"Kuncak","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Philippe","family":"Suter","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"A\u00eft-Kaci, H.: Warren\u2019s Abstract Machine: A Tutorial Reconstruction. MIT Press (1991) (available online as PDF)","DOI":"10.7551\/mitpress\/7160.001.0001"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Baader, F., Snyder, W.: Unification theory. In: Handbook of Automated Reasoning. Elsevier (2001)","DOI":"10.1016\/B978-044450813-3\/50010-2"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Flener, P.: Logic Program Synthesis from Incomplete Information. Kluwer Academic Publishers (1995)","DOI":"10.1007\/978-1-4615-2205-8"},{"key":"8_CR4","unstructured":"Hamza, J., Jobstmann, B., Kuncak, V.: Synthesis for regular specifications over unbounded domains. In: FMCAD, pp. 101\u2013109 (2010)"},{"key":"8_CR5","unstructured":"Hodges, W.: A Shorter Model Theory. Cambridge University Press (1997)"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Jobstmann, B., Bloem, R.: Optimizations for ltl synthesis. In: FMCAD, pp. 117\u2013124 (2006)","DOI":"10.1109\/FMCAD.2006.22"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"K\u00f6ksal, A.S., Kuncak, V., Suter, P.: Constraints as control. In: POPL, pp. 151\u2013164 (2012)","DOI":"10.1145\/2103621.2103675"},{"issue":"2","key":"8_CR8","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1145\/2076450.2076472","volume":"55","author":"V. Kuncak","year":"2012","unstructured":"Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Software synthesis procedures. CACM\u00a055(2), 103\u2013111 (2012)","journal-title":"CACM"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Complete functional synthesis. In: PLDI, pp. 316\u2013329 (2010)","DOI":"10.1145\/1809028.1806632"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/11513988_5","volume-title":"Computer Aided Verification","author":"S.K. Lahiri","year":"2005","unstructured":"Lahiri, S.K., Ball, T., Cook, B.: Predicate Abstraction via Symbolic Decision Procedures. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 24\u201338. Springer, Heidelberg (2005)"},{"issue":"3","key":"8_CR11","doi-asserted-by":"crossref","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. CACM\u00a014(3), 151\u2013165 (1971)","journal-title":"CACM"},{"issue":"1","key":"8_CR12","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1145\/357084.357090","volume":"2","author":"Z. Manna","year":"1980","unstructured":"Manna, Z., Waldinger, R.J.: A deductive approach to program synthesis. TOPLAS\u00a02(1), 90\u2013121 (1980)","journal-title":"TOPLAS"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"Maranget, L.: Compiling pattern matching to good decision trees. In: ML, pp. 35\u201346 (2008)","DOI":"10.1145\/1411304.1411311"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Generalized, efficient array decision procedures. In: FMCAD, pp. 45\u201352 (2009)","DOI":"10.1109\/FMCAD.2009.5351142"},{"issue":"2","key":"8_CR15","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. TOPLAS\u00a01(2), 245\u2013257 (1979)","journal-title":"TOPLAS"},{"issue":"9","key":"8_CR16","first-page":"1024","volume":"16","author":"D.R. Smith","year":"1990","unstructured":"Smith, D.R.: KIDS: A semiautomatic program development system. TSE\u00a016(9), 1024\u20131043 (1990)","journal-title":"TSE"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Tancau, L., Bod\u00edk, R., Seshia, S.A., Saraswat, V.A.: Combinatorial sketching for finite programs. In: ASPLOS, pp. 404\u2013415 (2006)","DOI":"10.1145\/1168918.1168907"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Spielmann, A., Kuncak, V.: Synthesis for unbounded bit-vector arithmetic. In: IJCAR, pp. 499\u2013513 (2012)","DOI":"10.1007\/978-3-642-31365-3_39"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Srivastava, S., Gulwani, S., Foster, J.S.: From program verification to program synthesis. In: POPL, pp. 313\u2013326 (2010)","DOI":"10.1145\/1707801.1706337"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"Stump, A., Barrett, C.W., Dill, D.L., Levitt, J.R.: A decision procedure for an extensional theory of arrays. In: LICS, pp. 29\u201337 (2001)","DOI":"10.1109\/LICS.2001.932480"},{"key":"8_CR21","unstructured":"Sturm, T., Weispfenning, V.: Quantifier elimination in term algebras: The case of finite languages. In: Ganzha, V.G., Mayr, E.W., Vorozhtsov, E.V. (eds.) Computer Algebra in Scientific Computing (CASC). TUM M\u00fcnchen (2002)"},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"Vechev, M.T., Yahav, E., Yorsh, G.: Abstraction-guided synthesis of synchronization. In: POPL, pp. 327\u2013338 (2010)","DOI":"10.1145\/1707801.1706338"},{"key":"8_CR23","unstructured":"Wadler, P.: The Implementation of Functional Programming Languages: Efficient Compilation of Pattern-matching, ch. 5, pp. 78\u2013103 (1987)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-35873-9_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,29]],"date-time":"2025-04-29T15:33:52Z","timestamp":1745940832000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-35873-9_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642358722","9783642358739"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-35873-9_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}