{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T09:46:10Z","timestamp":1769766370123,"version":"3.49.0"},"publisher-location":"Cham","reference-count":26,"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_22","type":"book-chapter","created":{"date-parts":[[2015,7,13]],"date-time":"2015-07-13T11:08:53Z","timestamp":1436785733000},"page":"377-394","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["Adaptive Concretization for Parallel Program Synthesis"],"prefix":"10.1007","author":[{"given":"Jinseong","family":"Jeon","sequence":"first","affiliation":[]},{"given":"Xiaokang","family":"Qiu","sequence":"additional","affiliation":[]},{"given":"Armando","family":"Solar-Lezama","sequence":"additional","affiliation":[]},{"given":"Jeffrey S.","family":"Foster","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,14]]},"reference":[{"key":"22_CR1","unstructured":"Alur, R., Bod\u00edk, R., Juniwal, G., Martin, M.M.K., Raghothaman, M., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-guided synthesis. In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20\u201323, 2013, pp. 1\u201317 (2013). \n                      http:\/\/ieeexplore.ieee.org\/xpl\/freeabs_all.jsp?arnumber=6679385"},{"key":"22_CR2","unstructured":"Ansel, J., Kamil, S., Veeramachaneni, K., Ragan-Kelley, J., Bosboom, J., O\u2019Reilly, U., Amarasinghe, S.P.: Opentuner: an extensible framework for program autotuning. In: International Conference on Parallel Architectures and Compilation, PACT 2014, Edmonton, AB, Canada, August 24\u201327, 2014, pp. 303\u2013316. (2014). \n                      http:\/\/doi.acm.org\/10.1145\/2628071.2628092"},{"key":"22_CR3","unstructured":"Chaganty, A., Nori, A.V., Rajamani, S.K.: Efficiently sampling probabilistic programs via program analysis. In: Proceedings of the Sixteenth International Conference on Artificial Intelligence and Statistics, AISTATS 2013, Scottsdale, AZ, USA, April 29 - May 1, 2013, pp. 153\u2013160 (2013). \n                      http:\/\/jmlr.org\/proceedings\/papers\/v31\/chaganty13a.html"},{"key":"22_CR4","unstructured":"Chaudhuri, S., Clochard, M., Solar-Lezama, A.: Bridging boolean and quantitative synthesis using smoothed proof search. In: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, San Diego, CA, USA, January 20\u201321, 2014, pp. 207\u2013220 (2014). \n                      http:\/\/doi.acm.org\/10.1145\/2535838.2535859"},{"key":"22_CR5","unstructured":"Chaudhuri, S., Solar-Lezama, A.: Smooth interpretation. In: Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2010, Toronto, Ontario, Canada, June 5\u201310 2010, pp. 279\u2013291 (2010). \n                      http:\/\/doi.acm.org\/10.1145\/1806596.1806629"},{"key":"22_CR6","unstructured":"Cheung, A., Solar-Lezama, A., Madden, S.: Optimizing database-backed applications with query synthesis. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2013, Seattle, WA, USA, June 16\u201319, 2013, pp. 3\u201314 (2013). \n                      http:\/\/doi.acm.org\/10.1145\/2462156.2462180"},{"key":"22_CR7","unstructured":"Gaudin, W., Mallinson, A., Perks, O., Herdman, J., Beckingsale, D., Levesque, J., Jarvis, S.: Optimising hydrodynamics applications for the cray xc30 with the application tool suite. The Cray User Group, pp. 4\u20138 (2014)"},{"key":"22_CR8","unstructured":"Gulwani, S.: Automating string processing in spreadsheets using input-output examples. In: Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26\u201328, 2011, pp. 317\u2013330 (2011). \n                      http:\/\/doi.acm.org\/10.1145\/1926385.1926423"},{"issue":"4","key":"22_CR9","first-page":"245","volume":"6","author":"Y Hamadi","year":"2009","unstructured":"Hamadi, Y., Jabbour, S., Sais, L.: Manysat: a parallel SAT solver. JSAT 6(4), 245\u2013262 (2009). \n                      http:\/\/jsat.ewi.tudelft.nl\/content\/volume6\/JSAT6_12_Hamadi.pdf","journal-title":"JSAT"},{"key":"22_CR10","unstructured":"Harris, W.R., Gulwani, S.: Spreadsheet table transformations from examples. In: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, June 4\u20138, 2011, pp. 317\u2013328 (2011). \n                      http:\/\/doi.acm.org\/10.1145\/1993498.1993536"},{"key":"22_CR11","unstructured":"Jeon, J., Qiu, X., Foster, J.S., Solar-Lezama, A.: Synthesizing Framework Models for Symbolic Execution, under submission"},{"key":"22_CR12","unstructured":"Jha, S., Gulwani, S., Seshia, S.A., Tiwari, A.: Oracle-guided component-based program synthesis. In: Proceedings of the 32nd ACM\/IEEE International Conference on Software Engineering, Vol. 1, ICSE 2010, pp. 215\u2013224. ACM, New York (2010). \n                      http:\/\/doi.acm.org\/10.1145\/1806799.1806833"},{"key":"22_CR13","unstructured":"Qiu, X., Solar-Lezama, A.: Synthesizing Data-Structure Manipulations with Natural Proofs, under submission"},{"key":"22_CR14","unstructured":"Schkufza, E., Sharma, R., Aiken, A.: Stochastic superoptimization. In: Architectural Support for Programming Languages and Operating Systems, ASPLOS 2013, Houston, TX, USA - March 16\u201320, 2013, pp. 305\u2013316 (2013). \n                      http:\/\/doi.acm.org\/10.1145\/2451116.2451150"},{"key":"22_CR15","unstructured":"Schkufza, E., Sharma, R., Aiken, A.: Stochastic optimization of floating-point programs with tunable precision. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014, Edinburgh, United Kingdom - June 09\u201311, 2014. p. 9 (2014). \n                      http:\/\/doi.acm.org\/10.1145\/2594291.2594302"},{"key":"22_CR16","doi-asserted-by":"crossref","unstructured":"Sharma, R., Aiken, A.: From invariant checking to invariant inference using randomized search. In: Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18\u201322, 2014, Proceedings, pp. 88\u2013105 (2014). \n                      http:\/\/dx.doi.org\/10.1007\/978-3-319-08867-9_6","DOI":"10.1007\/978-3-319-08867-9_6"},{"key":"22_CR17","doi-asserted-by":"crossref","unstructured":"Singh, R., Gulwani, S.: Synthesizing number transformations from input-output examples. In: Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7\u201313, 2012 , Proceedings, pp. 634\u2013651 (2012). \n                      http:\/\/dx.doi.org\/10.1007\/978-3-642-31424-7_44","DOI":"10.1007\/978-3-642-31424-7_44"},{"key":"22_CR18","unstructured":"Singh, R., Gulwani, S., Solar-Lezama, A.: Automated feedback generation for introductory programming assignments. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2013, Seattle, WA, USA, June 16\u201319 2013, pp. 15\u201326 (2013). \n                      http:\/\/doi.acm.org\/10.1145\/2462156.2462195"},{"issue":"5\u20136","key":"22_CR19","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. Int. J. Softw. Tools Technol. Transf. 15(5\u20136), 475\u2013495 (2013)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"22_CR20","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Jones, C.G., Bodik, R.: Sketching concurrent data structures. In: Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation, PLDI 2008, pp. 136\u2013148 (2008)","DOI":"10.1145\/1375581.1375599"},{"key":"22_CR21","unstructured":"Torlak, E., Bod\u00edk, R.: A lightweight symbolic virtual machine for solver-aided host languages. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014, Edinburgh, United Kingdom - June 09\u201311, 2014, p. 54 (2014). \n                      http:\/\/doi.acm.org\/10.1145\/2594291.2594340"},{"key":"22_CR22","unstructured":"Udupa, A., Raghavan, A., Deshmukh, J.V., Mador-Haim, S., Martin, M.M.K., Alur, R.: TRANSIT: specifying protocols with concolic snippets. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2013, Seattle, WA, USA, June 16\u201319, 2013, pp. 287\u2013296 (2013). \n                      http:\/\/doi.acm.org\/10.1145\/2462156.2462174"},{"key":"22_CR23","unstructured":"Vechev, M.T., Yahav, E.: Deriving linearizable fine-grained concurrent objects. In: Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, June 7\u201313, 2008, pp. 125\u2013135 (2008). \n                      http:\/\/doi.acm.org\/10.1145\/1375581.1375598"},{"issue":"6","key":"22_CR24","doi-asserted-by":"publisher","first-page":"80","DOI":"10.2307\/3001968","volume":"1","author":"F Wilcoxon","year":"1945","unstructured":"Wilcoxon, F.: Individual comparisons by ranking methods. Biometrics Bull. 1(6), 80\u201383 (1945)","journal-title":"Biometrics Bull."},{"key":"22_CR25","doi-asserted-by":"crossref","unstructured":"Wintersteiger, C.M., Hamadi, Y., de Moura, L.M.: A concurrent portfolio approach to SMT solving. In: Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009, Proceedings, pp. 715\u2013720 (2009). \n                      http:\/\/dx.doi.org\/10.1007\/978-3-642-02658-4_60","DOI":"10.1007\/978-3-642-02658-4_60"},{"issue":"4\u20136","key":"22_CR26","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1006\/jsco.1996.0030","volume":"21","author":"H Zhang","year":"1996","unstructured":"Zhang, H., Bonacina, M.P., Hsiang, J.: Psato: A distributed propositional prover and its application to quasigroup problems. J. Symb. Comput. 21(4\u20136), 543\u2013560 (1996). \n                      http:\/\/dx.doi.org\/10.1006\/jsco.1996.0030","journal-title":"J. Symb. Comput."}],"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_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,22]],"date-time":"2019-07-22T20:15:48Z","timestamp":1563826548000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-21668-3_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319216676","9783319216683"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21668-3_22","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"}}]}}