{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T02:50:52Z","timestamp":1781059852296,"version":"3.54.1"},"reference-count":24,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2012,2,1]],"date-time":"2012-02-01T00:00:00Z","timestamp":1328054400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Commun. ACM"],"published-print":{"date-parts":[[2012,2]]},"abstract":"<jats:p>\n            Automated synthesis of program fragments from specifications can make programs easier to write and easier to reason about. To integrate synthesis into programming languages, software synthesis algorithms should behave in a predictable way: they should succeed for a well-defined class of specifications. We propose to systematically generalize decision procedures into\n            <jats:italic>synthesis procedures<\/jats:italic>\n            , and use them to compile implicitly specified computations embedded inside functional and imperative programs. Synthesis procedures are predictable, because they are guaranteed to find code that satisfies the specification whenever such code exists. To illustrate our method, we derive synthesis procedures by extending quantifier elimination algorithms for integer arithmetic and set data structures. We then show that an implementation of such synthesis procedures can extend a compiler to support implicit value definitions and advanced pattern matching.\n          <\/jats:p>","DOI":"10.1145\/2076450.2076472","type":"journal-article","created":{"date-parts":[[2012,1,24]],"date-time":"2012-01-24T16:47:14Z","timestamp":1327423634000},"page":"103-111","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":28,"title":["Software synthesis procedures"],"prefix":"10.1145","volume":"55","author":[{"given":"Viktor","family":"Kuncak","sequence":"first","affiliation":[{"name":"Swiss Federal Institute of Technology (EPFL), Lausanne, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mika\u00ebl","family":"Mayer","sequence":"additional","affiliation":[{"name":"Swiss Federal Institute of Technology (EPFL), Lausanne, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ruzica","family":"Piskac","sequence":"additional","affiliation":[{"name":"Swiss Federal Institute of Technology (EPFL), Lausanne, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Philippe","family":"Suter","sequence":"additional","affiliation":[{"name":"Swiss Federal Institute of Technology (EPFL), Lausanne, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2012,2]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/1324777"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-02945-9"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_1_4_1","volume-title":"A Discipline of Programming","author":"Dijkstra E.W.","year":"1976","unstructured":"Dijkstra , E.W. A Discipline of Programming . Prentice-Hall, Inc. , Upper Saddle River, NJ, 1976 . Dijkstra, E.W. A Discipline of Programming. Prentice-Hall, Inc., Upper Saddle River, NJ, 1976."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0062837"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512558"},{"key":"e_1_2_1_7_1","volume-title":"CAV","author":"Ganzinger H.","year":"2004","unstructured":"Ganzinger , H. , Hagen , G. , Nieuwenhuis , R. , Oliveras , A. , Tinelli , C. DPLL(T) : Fast decision procedures . In CAV ( 2004 ), 175--188. Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C. DPLL(T): Fast decision procedures. In CAV (2004), 175--188."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/1624562.1624585"},{"key":"e_1_2_1_9_1","volume-title":"FMCAD","author":"Hamza J.","year":"2010","unstructured":"Hamza , J. , Jobstmann , B. , Kuncak , V. Synthesis for regular specifications over unbounded domains . In FMCAD , 2010 . Hamza, J., Jobstmann, B., Kuncak, V. Synthesis for regular specifications over unbounded domains. In FMCAD, 2010."},{"key":"e_1_2_1_10_1","first-page":"20","volume":"1","author":"Jaffar J.","year":"1994","unstructured":"Jaffar , J. , Maher , M.J. Constraint logic programming: A survey. J. Log. Program , 1 9\/ 20 ( 1994 ), 503--581. Jaffar, J., Maher, M.J. Constraint logic programming: A survey. J. Log. Program, 19\/20 (1994), 503--581.","journal-title":"J. Log. Program"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1186632.1186633"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806632"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-006-9042-1"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/1887459.1887465"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/362566.362568"},{"key":"e_1_2_1_16_1","volume-title":"Programming in Scala: A Comprehensive Step-By-Step Guide","author":"Odersky M.","year":"2008","unstructured":"Odersky , M. , Spoon , L. , Venners , B. Programming in Scala: A Comprehensive Step-By-Step Guide . Artima Press , Mountain View, CA , 2008 . Odersky, M., Spoon, L., Venners, B. Programming in Scala: A Comprehensive Step-By-Step Guide. Artima Press, Mountain View, CA, 2008."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512776"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_25"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75293"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/135226.135233"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168907"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706337"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706325"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375624"}],"container-title":["Communications of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2076450.2076472","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2076450.2076472","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T09:48:24Z","timestamp":1750240104000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2076450.2076472"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,2]]},"references-count":24,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2012,2]]}},"alternative-id":["10.1145\/2076450.2076472"],"URL":"https:\/\/doi.org\/10.1145\/2076450.2076472","relation":{},"ISSN":["0001-0782","1557-7317"],"issn-type":[{"value":"0001-0782","type":"print"},{"value":"1557-7317","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,2]]},"assertion":[{"value":"2012-02-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}