{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:47:59Z","timestamp":1772164079498,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":65,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,6,2]],"date-time":"2017-06-02T00:00:00Z","timestamp":1496361600000},"content-version":"vor","delay-in-days":365,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000015","name":"U.S. Department of Energy","doi-asserted-by":"publisher","award":["DE-SC0008923, DE- SC0005288"],"award-info":[{"award-number":["DE-SC0008923, DE- SC0005288"]}],"id":[{"id":"10.13039\/100000015","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,6,2]]},"DOI":"10.1145\/2908080.2908117","type":"proceedings-article","created":{"date-parts":[[2016,6,2]],"date-time":"2016-06-02T15:23:42Z","timestamp":1464881022000},"page":"711-726","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":41,"title":["Verified lifting of stencil computations"],"prefix":"10.1145","author":[{"given":"Shoaib","family":"Kamil","sequence":"first","affiliation":[{"name":"Adobe, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alvin","family":"Cheung","sequence":"additional","affiliation":[{"name":"University of Washington, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shachar","family":"Itzhaky","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Armando","family":"Solar-Lezama","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2016,6,2]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Apache Hive. http:\/\/hive.apache.org."},{"key":"e_1_3_2_1_2_1","unstructured":"Syntax-Guided Synthesis Competition. http:\/\/www.sygus. org."},{"key":"e_1_3_2_1_3_1","first-page":"17","volume-title":"FMCAD 2013","author":"Alur Rajeev","year":"2013","unstructured":"Rajeev Alur, Rastislav Bod\u00b4\u0131k, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. Syntax-guided synthesis. In Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013, pages 1\u201317, 2013."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/645671.665527"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628071.2628092"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/125826.125925"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2442516.2442529"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01008348"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/263580.263662"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/1946284.1946291"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/11609773_28"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11486-1_35"},{"key":"e_1_3_2_1_13_1","volume-title":"Workshop on Programmable Models for Emerging Architecture (PMEA)","author":"Catanzaro Bryan","year":"2009","unstructured":"Bryan Catanzaro, Shoaib Kamil, Yunsup Lee, Krste Asanovic, James Demmel, Kurt Keutzer, John Shalf, Kathy Yelick, and Armando Fox. SEJITS: Getting productivity and performance with selective embedded JIT specialization. In Workshop on Programmable Models for Emerging Architecture (PMEA), 2009."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1177\/1094342007078442"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462180"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/IPDPS.2011.70"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_23"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/1413370.1413375"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/646778.704483"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/302405.302467"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/49418"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503291"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1088149.1088197"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_5"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2544137.2544160"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129626414410023"},{"key":"e_1_3_2_1_28_1","volume-title":"Sandia National Laboratory","author":"Heroux Michael A.","year":"2009","unstructured":"Michael A. Heroux, Douglas W. Doerfler, Paul S. Crozier, James M. Willenbring, H. Carter Edwards, Alan Williams, Mahesh Rajan, Eric R. Keiter, Heidi K. Thornquist, and Robert W. Numrich. Improving performance via mini-applications. Technical report, Sandia National Laboratory, 2009."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_1_30_1","unstructured":"Intel. The X10 parallel programming language. http:\/\/ x10-lang.org."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73588"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1755913.1755939"},{"key":"e_1_3_2_1_33_1","first-page":"394","volume-title":"CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II","author":"Jeon Jinseong","year":"2015","unstructured":"Jinseong Jeon, Xiaokang Qiu, Armando Solar-Lezama, and Jeffrey S. Foster. Adaptive concretization for parallel program synthesis. In Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II, pages 377\u2013394, 2015."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/543552.512566"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2110170.2110185"},{"key":"e_1_3_2_1_36_1","volume-title":"Workshop on Optimizing Stencil Computations","author":"Kamil Shoaib","year":"2013","unstructured":"Shoaib Kamil. A cross-domain stencil benchmark suite. In Workshop on Optimizing Stencil Computations, 2013."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/IPDPS.2010.5470421"},{"key":"e_1_3_2_1_38_1","first-page":"602","volume-title":"CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I","author":"Karbyshev Aleksandr","year":"2015","unstructured":"Aleksandr Karbyshev, Nikolaj Bj\u00f8rner, Shachar Itzhaky, Noam Rinetzky, and Sharon Shoham. Property-directed inference of universal invariants or proving their absence. In Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, pages 583\u2013602, 2015."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462187"},{"key":"e_1_3_2_1_40_1","volume-title":"Cloverleaf: Preparing hydrodynamics codes for exascale","author":"Mallinson A.C.","year":"2013","unstructured":"A.C. Mallinson, D.A. Beckingsale, W.P. Gaudin, J.A. Herdman, J.M. Levesque, and S.A. Jarvis. Cloverleaf: Preparing hydrodynamics codes for exascale. In Cray User Group, 2013."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/36206.36194"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/11916277_25"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737974"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2694344.2694364"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594339"},{"issue":"1","key":"e_1_3_2_1_46_1","first-page":"153","article-title":"A note on inductive generalization","volume":"5","author":"Plotkin Gordon D","year":"1970","unstructured":"Gordon D Plotkin. A note on inductive generalization. Machine Intelligence, 5(1):153\u2013163, 1970.","journal-title":"Machine Intelligence"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462176"},{"key":"e_1_3_2_1_48_1","volume-title":"Edinburgh University Press","author":"Reynolds John C.","year":"1969","unstructured":"John C. Reynolds. Transformational systems and the algebraic structure of atomic formulas. In Bernard Meltzer and Donald Michie, editors, Machine Intelligence 5, pages 135\u2013151. Edinburgh University Press, Edinburgh, Scotland, 1969."},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.5555\/370049.370403"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2490301.2451150"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594302"},{"key":"e_1_3_2_1_52_1","unstructured":"Armando Solar Lezama. Program Synthesis By Sketching. PhD thesis EECS Department University of California Berkeley Dec 2008."},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250754"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168907"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2584665"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/1989493.1989508"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462174"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1080\/10407782.2014.894387"},{"key":"e_1_3_2_1_59_1","volume-title":"OpenMP parallel acceleration of a 3D finite","author":"Vasco Diego","year":"2011","unstructured":"Diego Vasco, Nelson Moraga, Aurel Neic, and Gundolf Haase. OpenMP parallel acceleration of a 3D finite volume method based code for simulation of non-Newtonian fluid flows. In Sergio Guti\u00e9rrez, Daniel Hurtado, and Esteban S\u00e1ez, editors, Cuadernos de Mec\u00e1nica Computacional, pages 108\u2013117, Concepci\u00b4on, Chile, 2011. Sociedad Chilena de Mec\u00e1nica Computacional."},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/1449764.1449767"},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.5555\/151145"},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.5555\/1998496.1998539"},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1015460304860"},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.5555\/2228298.2228301"},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2004.1274043"}],"event":{"name":"PLDI '16: ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Santa Barbara CA USA","acronym":"PLDI '16","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2908080.2908117","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2908080.2908117","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2908080.2908117","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T09:19:30Z","timestamp":1763457570000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2908080.2908117"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,6,2]]},"references-count":65,"alternative-id":["10.1145\/2908080.2908117","10.1145\/2908080"],"URL":"https:\/\/doi.org\/10.1145\/2908080.2908117","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2980983.2908117","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2016,6,2]]},"assertion":[{"value":"2016-06-02","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}