{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:47:04Z","timestamp":1772164024312,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":38,"publisher":"ACM","license":[{"start":{"date-parts":[[2011,6,4]],"date-time":"2011-06-04T00:00:00Z","timestamp":1307145600000},"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":[],"published-print":{"date-parts":[[2011,6,4]]},"DOI":"10.1145\/1993498.1993506","type":"proceedings-article","created":{"date-parts":[[2011,6,6]],"date-time":"2011-06-06T07:53:52Z","timestamp":1307346832000},"page":"62-73","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":189,"title":["Synthesis of loop-free programs"],"prefix":"10.1145","author":[{"given":"Sumit","family":"Gulwani","sequence":"first","affiliation":[{"name":"Microsoft Research, Redmond, Washington, USA"}]},{"given":"Susmit","family":"Jha","sequence":"additional","affiliation":[{"name":"University of California, Berkeley, California, USA"}]},{"given":"Ashish","family":"Tiwari","sequence":"additional","affiliation":[{"name":"SRI International, Menlo Park, USA"}]},{"given":"Ramarathnam","family":"Venkatesan","sequence":"additional","affiliation":[{"name":"Microsoft Research, Redmond, Washington, USA"}]}],"member":"320","published-online":{"date-parts":[[2011,6,4]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Satisfiability modulo theories competition (smt-comp). \\URLhttp:\/\/www.smtcomp.org\/2009\/index.shtml. Satisfiability modulo theories competition (smt-comp). \\URLhttp:\/\/www.smtcomp.org\/2009\/index.shtml."},{"key":"e_1_3_2_1_2_1","unstructured":"SMTLIB : Satisfiability modulo theories lib. URLhttp:\/\/smtlib.org. SMTLIB: Satisfiability modulo theories lib. URLhttp:\/\/smtlib.org."},{"key":"e_1_3_2_1_3_1","unstructured":"Yices: An SMT solver. URLhttp:\/\/yices.csl.sri.com. Yices: An SMT solver. URLhttp:\/\/yices.csl.sri.com."},{"key":"e_1_3_2_1_4_1","volume-title":"Download: URLhttp:\/\/www.hackersdelight.org\/aha.zip","author":"Hacker's The","year":"2008","unstructured":"The AHA! (A Hacker's Assistant) Superoptimizer , 2008 . Download: URLhttp:\/\/www.hackersdelight.org\/aha.zip , Documentation : URLhttp :\/\/www.hackersdelight.org\/aha\/aha.pdf. The AHA! (A Hacker's Assistant) Superoptimizer, 2008. Download: URLhttp:\/\/www.hackersdelight.org\/aha.zip, Documentation: URLhttp:\/\/www.hackersdelight.org\/aha\/aha.pdf."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168906"},{"key":"e_1_3_2_1_6_1","volume-title":"OSDI","author":"Bansal S.","year":"2008","unstructured":"S. Bansal and A. Aiken . Binary translation using peephole superoptimizers . In OSDI , 2008 . S. Bansal and A. Aiken. Binary translation using peephole superoptimizers. In OSDI, 2008."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75280"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004562"},{"key":"e_1_3_2_1_9_1","volume-title":"LOBSTR.","author":"Flener P.","year":"1994","unstructured":"P. Flener and L. Popelmnsky . On the use of inductive reasoning in program synthesis: Prejudice and prospects . In LOBSTR. 1994 . P. Flener and L. Popelmnsky. On the use of inductive reasoning in program synthesis: Prejudice and prospects. In LOBSTR. 1994."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(67)91165-5"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/143095.143146"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1836089.1836091"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926423"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993505"},{"key":"e_1_3_2_1_15_1","volume-title":"FMCAD","author":"Hamza J.","year":"2010","unstructured":"J. Hamza , B. Jobstmann , and V. Kuncak . Synthesis for regular specifications over unbounded domains . In FMCAD , 2010 . J. Hamza, B. Jobstmann, and V. Kuncak. Synthesis for regular specifications over unbounded domains. In FMCAD, 2010."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993536"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1869459.1869463"},{"key":"e_1_3_2_1_18_1","first-page":"293","volume-title":"Watch what I do: programming by demonstration","author":"Jackiw R. N.","year":"1993","unstructured":"R. N. Jackiw and W. F. Finzer . The geometer's sketchpad: programming by geometry . In Watch what I do: programming by demonstration , pages 293 -- 307 . MIT Press , 1993 . R. N. Jackiw and W. F. Finzer. The geometer's sketchpad: programming by geometry. In Watch what I do: programming by demonstration, pages 293--307. MIT Press, 1993."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806799.1806833"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1795194.1795198"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134003"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512566"},{"key":"e_1_3_2_1_23_1","unstructured":"D. E. Knuth. The art of computer programming. \\URLhttp:\/\/www-cs-faculty.stanford.edu\/ knuth\/taocp.html. D. E. Knuth. The art of computer programming. \\URLhttp:\/\/www-cs-faculty.stanford.edu\/ knuth\/taocp.html."},{"key":"e_1_3_2_1_24_1","volume-title":"ICML","author":"Lau T. A.","year":"2000","unstructured":"T. A. Lau , P. Domingos , and D. S. Weld . Version space algebra and its application to programming by demonstration . In ICML , 2000 . T. A. Lau, P. Domingos, and D. S. Weld. Version space algebra and its application to programming by demonstration. In ICML, 2000."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/3266641.3266682"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065018"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/357084.357090"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/36206.36194"},{"key":"e_1_3_2_1_29_1","series-title":"The APIC Series","volume-title":"Inductive Logic Programming","author":"Muggleton S.","year":"1992","unstructured":"S. Muggleton , editor. Inductive Logic Programming , volume 38 of The APIC Series . Academic Press , 1992 . S. Muggleton, editor. Inductive Logic Programming, volume 38 of The APIC Series. Academic Press, 1992."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/1192.001.0001","volume-title":"Algorithmic Program DeBugging","author":"Shapiro E. Y.","year":"1983","unstructured":"E. Y. Shapiro . Algorithmic Program DeBugging . MIT Press , Cambridge, MA, USA , 1983 . E. Y. Shapiro. Algorithmic Program DeBugging. MIT Press, Cambridge, MA, USA, 1983."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250754"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065045"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168907"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706337"},{"key":"e_1_3_2_1_35_1","unstructured":"M. Stickel R. Waldinger M. Lowry T. Pressburger and I. Underwood. Deductive composition of astro. software from subroutine libraries. In CADE '94. M. Stickel R. Waldinger M. Lowry T. Pressburger and I. Underwood. Deductive composition of astro. software from subroutine libraries. In CADE '94."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-93900-9_25"},{"key":"e_1_3_2_1_37_1","unstructured":"H. S. Warren. Hacker's Delight. Addison-Wesley '02. H. S. Warren. Hacker's Delight. Addison-Wesley '02."},{"key":"e_1_3_2_1_38_1","first-page":"293","volume-title":"Watch what I do: programming by demonstration","author":"Witten I. H.","year":"1993","unstructured":"I. H. Witten and D. Mo . TELS: learning text editing tasks from examples . In Watch what I do: programming by demonstration , pages 293 -- 307 . MIT Press , Cambridge, MA, USA , 1993 . I. H. Witten and D. Mo. TELS: learning text editing tasks from examples. In Watch what I do: programming by demonstration, pages 293--307. MIT Press, Cambridge, MA, USA, 1993."}],"event":{"name":"PLDI '11: ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"San Jose California USA","acronym":"PLDI '11","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1993498.1993506","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1993498.1993506","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:05:46Z","timestamp":1750230346000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1993498.1993506"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,6,4]]},"references-count":38,"alternative-id":["10.1145\/1993498.1993506","10.1145\/1993498"],"URL":"https:\/\/doi.org\/10.1145\/1993498.1993506","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1993316.1993506","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2011,6,4]]},"assertion":[{"value":"2011-06-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}