{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T20:55:36Z","timestamp":1760043336602,"version":"3.37.3"},"reference-count":29,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2017,3,1]],"date-time":"2017-03-01T00:00:00Z","timestamp":1488326400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,3,1]],"date-time":"2017-03-01T00:00:00Z","timestamp":1488326400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100000143","name":"CCF","doi-asserted-by":"publisher","award":["1139021","1139056"],"award-info":[{"award-number":["1139021","1139056"]}],"id":[{"id":"10.13039\/100000143","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000143","name":"CCF","doi-asserted-by":"publisher","award":["1161775"],"award-info":[{"award-number":["1161775"]}],"id":[{"id":"10.13039\/100000143","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Laboratory of Telecommunication Sciences"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2017,3]]},"DOI":"10.1007\/s10703-017-0269-8","type":"journal-article","created":{"date-parts":[[2017,3,7]],"date-time":"2017-03-07T12:20:47Z","timestamp":1488889247000},"page":"75-95","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["An empirical study of adaptive concretization for parallel program synthesis"],"prefix":"10.1007","volume":"50","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":[[2017,3,7]]},"reference":[{"key":"269_CR1","doi-asserted-by":"crossref","unstructured":"Alur R, Bod\u00edk R, Juniwal G, Martin MMK, Raghothaman M, Seshia SA, Singh R, Solar-Lezama A, Torlak E, Udupa A (2013) Syntax-guided synthesis. In: Formal methods in computer-aided design, FMCAD 2013, Portland, OR, USA, October 20\u201323, 2013, pp 1\u201317","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"269_CR2","doi-asserted-by":"crossref","unstructured":"Ansel J, Kamil S, Veeramachaneni K, Ragan-Kelley J, Bosboom J, O\u2019Reilly U, Amarasinghe SP (2014) Opentuner: an extensible framework for program autotuning. In: International conference on parallel architectures and compilation, PACT \u201914, Edmonton, AB, Canada, August 24\u201327, 2014, pp 303\u2013316","DOI":"10.1145\/2628071.2628092"},{"key":"269_CR3","unstructured":"Chaganty A, Nori AV, Rajamani SK (2013) 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\u2013May 1, 2013, pp 153\u2013160"},{"key":"269_CR4","doi-asserted-by":"crossref","unstructured":"Chaudhuri S, Clochard M, Solar-Lezama, A (2014) Bridging boolean and quantitative synthesis using smoothed proof search. In: The 41st annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL \u201914, San Diego, CA, USA, January 20\u201321, 2014, pp 207\u2013220","DOI":"10.1145\/2535838.2535859"},{"key":"269_CR5","doi-asserted-by":"crossref","unstructured":"Chaudhuri S, Solar-Lezama A (2010) Smooth interpretation. In: Proceedings of the 2010 ACM SIGPLAN conference on programming language design and implementation, PLDI 2010, Toronto, ON, Canada, June 5\u201310, 2010, pp 279\u2013291","DOI":"10.1145\/1806596.1806629"},{"key":"269_CR6","doi-asserted-by":"crossref","unstructured":"Cheung A, Solar-Lezama A, Madden S (2013) Optimizing database-backed applications with query synthesis. In: ACM SIGPLAN conference on programming language design and implementation, PLDI \u201913, Seattle, WA, USA, June 16\u201319, 2013, pp 3\u201314","DOI":"10.1145\/2491956.2462180"},{"issue":"1","key":"269_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1214\/aos\/1176344552","volume":"7","author":"B Efron","year":"1979","unstructured":"Efron B (1979) Bootstrap methods: another look at the jackknife. Ann Stat 7(1):1\u201326","journal-title":"Ann Stat"},{"key":"269_CR8","unstructured":"Gaudin W, Mallinson A, Perks O, Herdman J, Beckingsale D, Levesque J, Jarvis S (2014) Optimising hydrodynamics applications for the cray xc30 with the application tool suite. The Cray User Group, pp 4\u20138"},{"key":"269_CR9","doi-asserted-by":"crossref","unstructured":"Gulwani S (2011) 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","DOI":"10.1145\/1926385.1926423"},{"issue":"4","key":"269_CR10","first-page":"245","volume":"6","author":"Y Hamadi","year":"2009","unstructured":"Hamadi Y, Jabbour S, Sais L (2009) Manysat: a parallel SAT solver. JSAT 6(4):245\u2013262","journal-title":"JSAT"},{"key":"269_CR11","unstructured":"Harris WR, Gulwani S (2011) 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"},{"key":"269_CR12","unstructured":"Jeon J, Qiu X, Fetter-Degges J, Foster JS, Solar-Lezama A synthesizing framework models for symbolic execution. (Under submission)"},{"key":"269_CR13","doi-asserted-by":"crossref","unstructured":"Jeon J, Qiu X, Solar-Lezama A, Foster JS (2015) Adaptive concretization for parallel program synthesis. In: Computer aided verification (CAV), volume 9207 of lecture notes in computer science, pp 377\u2013394, San Francisco, CA, USA, July 2015. Springer International Publishing","DOI":"10.1007\/978-3-319-21668-3_22"},{"key":"269_CR14","doi-asserted-by":"crossref","unstructured":"Jha S, Gulwani S, Seshia SA, Tiwari A (2010) Oracle-guided component-based program synthesis. In: Proceedings of the 32nd ACM\/IEEE international conference on software engineering - Vol 1, ICSE \u201910, pp 215\u2013224, New York, NY, USA, 2010. ACM","DOI":"10.1145\/1806799.1806833"},{"issue":"1","key":"269_CR15","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1214\/aoms\/1177730491","volume":"18","author":"HB Mann","year":"1947","unstructured":"Mann HB, Whitney DR (1947) On a test of whether one of two random variables is stochastically larger than the other. Ann Math Stat 18(1):50\u201360","journal-title":"Ann Math Stat"},{"key":"269_CR16","unstructured":"Qiu X, Solar-Lezama A synthesizing data-structure manipulations with natural proofs. (Under submission)"},{"key":"269_CR17","doi-asserted-by":"crossref","unstructured":"Schkufza E, Sharma R, Aiken A (2013) Stochastic superoptimization. In: Architectural support for programming languages and operating systems, ASPLOS \u201913, Houston, TX, USA, March 16\u201320, 2013, pp 305\u2013316","DOI":"10.1145\/2451116.2451150"},{"key":"269_CR18","doi-asserted-by":"crossref","unstructured":"Schkufza E, Sharma R, Aiken A (2014) Stochastic optimization of floating-point programs with tunable precision. In: ACM SIGPLAN conference on programming language design and implementation, PLDI \u201914, Edinburgh, UK, June 09\u201311, 2014, p 9","DOI":"10.1145\/2666356.2594302"},{"key":"269_CR19","doi-asserted-by":"crossref","unstructured":"Sharma R, Aiken A (2014) From invariant checking to invariant inference using randomized search. In: Computer aided verification\u201426th 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","DOI":"10.1007\/978-3-319-08867-9_6"},{"key":"269_CR20","doi-asserted-by":"crossref","unstructured":"Singh R, Gulwani S (2012) Synthesizing number transformations from input-output examples. In: Computer aided verification\u201424th international conference, CAV 2012, Berkeley, CA, USA, July 7\u201313, 2012 Proceedings, pp 634\u2013651","DOI":"10.1007\/978-3-642-31424-7_44"},{"key":"269_CR21","doi-asserted-by":"crossref","unstructured":"Singh R, Gulwani S, Solar-Lezama A (2013) Automated feedback generation for introductory programming assignments. In: ACM SIGPLAN conference on programming language design and implementation, PLDI \u201913, Seattle, WA, USA, June 16\u201319, 2013, pp 15\u201326","DOI":"10.1145\/2491956.2462195"},{"issue":"5\u20136","key":"269_CR22","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 (2013) Program sketching. Int J Softw Tools Technol Transf 15(5\u20136):475\u2013495","journal-title":"Int J Softw Tools Technol Transf"},{"key":"269_CR23","doi-asserted-by":"crossref","unstructured":"Solar-Lezama A, Jones CG, Bodik R (2008) Sketching concurrent data structures. In: Proceedings of the 2008 ACM SIGPLAN conference on programming language design and implementation, PLDI \u201908, pp 136\u2013148","DOI":"10.1145\/1375581.1375599"},{"key":"269_CR24","doi-asserted-by":"crossref","unstructured":"Torlak E, Bod\u00edk R (2014) A lightweight symbolic virtual machine for solver-aided host languages. In: ACM SIGPLAN conference on programming language design and implementation, PLDI \u201914, Edinburgh, United Kingdom, June 09\u201311, 2014, p 54","DOI":"10.1145\/2666356.2594340"},{"key":"269_CR25","doi-asserted-by":"crossref","unstructured":"Udupa A, Raghavan A, Deshmukh JV, Mador-Haim S, Martin MMK, Alur R (2013) TRANSIT: specifying protocols with concolic snippets. In: ACM SIGPLAN conference on programming language design and implementation, PLDI \u201913, Seattle, WA, USA, June 16\u201319, 2013, pp 287\u2013296","DOI":"10.1145\/2491956.2462174"},{"key":"269_CR26","unstructured":"Vechev MT, Yahav E (2008) 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"},{"issue":"6","key":"269_CR27","doi-asserted-by":"publisher","first-page":"80","DOI":"10.2307\/3001968","volume":"1","author":"F Wilcoxon","year":"1945","unstructured":"Wilcoxon F (1945) Individual comparisons by ranking methods. Biom Bullet 1(6):80\u201383","journal-title":"Biom Bullet"},{"key":"269_CR28","doi-asserted-by":"crossref","unstructured":"Wintersteiger CM, Hamadi Y, de Moura LM (2009) A concurrent portfolio approach to SMT solving. In: Computer aided verification, 21st international conference, CAV 2009, Grenoble, France, June 26\u2013July 2, 2009. Proceedings, pp 715\u2013720","DOI":"10.1007\/978-3-642-02658-4_60"},{"issue":"4\u20136","key":"269_CR29","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1006\/jsco.1996.0030","volume":"21","author":"H Zhang","year":"1996","unstructured":"Zhang H, Hsiang Bonacina MP, Psato J (1996) A distributed propositional prover and its application to quasigroup problems. J Symb Comput 21(4\u20136):543\u2013560","journal-title":"J Symb Comput"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0269-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-017-0269-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0269-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,17]],"date-time":"2020-05-17T15:44:05Z","timestamp":1589730245000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-017-0269-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,3]]},"references-count":29,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2017,3]]}},"alternative-id":["269"],"URL":"https:\/\/doi.org\/10.1007\/s10703-017-0269-8","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2017,3]]},"assertion":[{"value":"7 March 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}