{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T09:22:58Z","timestamp":1769764978128,"version":"3.49.0"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319216676","type":"print"},{"value":"9783319216683","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21668-3_10","type":"book-chapter","created":{"date-parts":[[2015,7,13]],"date-time":"2015-07-13T11:08:53Z","timestamp":1436785733000},"page":"163-179","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":37,"title":["Synthesis Through Unification"],"prefix":"10.1007","author":[{"given":"Rajeev","family":"Alur","sequence":"first","affiliation":[]},{"given":"Pavol","family":"\u010cern\u00fd","sequence":"additional","affiliation":[]},{"given":"Arjun","family":"Radhakrishna","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,14]]},"reference":[{"key":"10_CR1","unstructured":"SyGuS competition 2014. \n                      http:\/\/www.sygus.org\/SyGuS-COMP2014.html"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Bod\u00edk, R., Juniwal, G., Martin, M., Raghothaman, M., Seshia, S., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-guided synthesis. In: FMCAD, pp. 1\u201317 (2013)","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"10_CR3","unstructured":"Alur, R., \u010cern\u00fd, P., Radhakrishna, A.: Synthesis through unification. CoRR abs\/1505.05868 (2015). \n                      http:\/\/arxiv.org\/abs\/1104.4306"},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"Bloem, R., Hofferek, G., K\u00f6nighofer, B., K\u00f6nighofer, R., Au\u00dferlechner, S., Sp\u00f6rk, R.: Synthesis of synchronization using uninterpreted functions. In: FMCAD, pp. 35\u201342 (2014)","DOI":"10.1109\/FMCAD.2014.6987593"},{"issue":"5\u20136","key":"10_CR5","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/s10009-013-0287-9","volume":"15","author":"R Bod\u00edk","year":"2013","unstructured":"Bod\u00edk, R., Jobstmann, B.: Algorithmic program synthesis: introduction. STTT 15(5\u20136), 397\u2013411 (2013)","journal-title":"STTT"},{"key":"10_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"951","DOI":"10.1007\/978-3-642-39799-8_68","volume-title":"Computer Aided Verification","author":"P \u010cern\u00fd","year":"2013","unstructured":"\u010cern\u00fd, P., Henzinger, T.A., Radhakrishna, A., Ryzhyk, L., Tarrach, T.: Efficient synthesis for concurrency by semantics-preserving transformations. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 951\u2013967. Springer, Heidelberg (2013)"},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"568","DOI":"10.1007\/978-3-319-08867-9_38","volume-title":"Computer Aided Verification","author":"P \u010cern\u00fd","year":"2014","unstructured":"\u010cern\u00fd, P., Henzinger, T.A., Radhakrishna, A., Ryzhyk, L., Tarrach, T.: Regression-free synthesis for concurrency. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 568\u2013584. Springer, Heidelberg (2014)"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: An abstract interpretation framework for termination. In: POPL, pp. 245\u2013258 (2012)","DOI":"10.1145\/2103621.2103687"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL, pp. 84\u201396 (1978)","DOI":"10.1145\/512760.512770"},{"key":"10_CR11","unstructured":"Cousot, P., Cousot, R.: Relational abstract interpretation of higher order functional programs (extended abstract). In: JTASPEFT\/WSA, pp. 33\u201336 (1991)"},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"Gulwani, S.: Automating string processing in spreadsheets using input-output examples. In: POPL, pp. 317\u2013330 (2011)","DOI":"10.1145\/1925844.1926423"},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"Gupta, A., Henzinger, T., Radhakrishna, A., Samanta, R., Tarrach, T.: Succinct representation of concurrent trace sets. In: POPL15, pp. 433\u2013444 (2015)","DOI":"10.1145\/2775051.2677008"},{"key":"10_CR14","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":"10_CR15","unstructured":"Lau, T., Domingos, P., Weld, D.: Version space algebra and its application to programming by demonstration. In: ICML, pp. 527\u2013534 (2000)"},{"issue":"5\u20136","key":"10_CR16","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/s10009-012-0249-7","volume":"15","author":"A Solar-Lezama","year":"2013","unstructured":"Solar-Lezama, A.: Program sketching. STTT 15(5\u20136), 475\u2013495 (2013)","journal-title":"STTT"},{"key":"10_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":"10_CR18","doi-asserted-by":"crossref","unstructured":"Udupa, A., Raghavan, A., Deshmukh, J.V., Mador-Haim, S., Martin, M.M.K., Alur, R.: TRANSIT: specifying protocols with concolic snippets. In: PLDI, pp. 287\u2013296 (2013)","DOI":"10.1145\/2499370.2462174"},{"key":"10_CR19","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":"10_CR20","volume-title":"Hacker\u2019s Delight","author":"HS Warren","year":"2002","unstructured":"Warren, H.S.: Hacker\u2019s Delight. Addison-Wesley Longman Publishing Co., Inc., Boston (2002)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21668-3_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,22]],"date-time":"2019-07-22T20:13:47Z","timestamp":1563826427000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-21668-3_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319216676","9783319216683"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21668-3_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"14 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}