{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:16:08Z","timestamp":1763468168810},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642540127"},{"type":"electronic","value":"9783642540134"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54013-4_22","type":"book-chapter","created":{"date-parts":[[2014,1,2]],"date-time":"2014-01-02T20:08:09Z","timestamp":1388693289000},"page":"395-414","source":"Crossref","is-referenced-by-count":13,"title":["Modular Synthesis of Sketches Using Models"],"prefix":"10.1007","author":[{"given":"Rohit","family":"Singh","sequence":"first","affiliation":[]},{"given":"Rishabh","family":"Singh","sequence":"additional","affiliation":[]},{"given":"Zhilei","family":"Xu","sequence":"additional","affiliation":[]},{"given":"Rebecca","family":"Krosnick","sequence":"additional","affiliation":[]},{"given":"Armando","family":"Solar-Lezama","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"22_CR1","doi-asserted-by":"crossref","unstructured":"Barthe, G., Crespo, J.M., Gulwani, S., Kunz, C., Marron, M.: From relational verification to simd loop synthesis. In: PPoPP (2013)","DOI":"10.1145\/2442516.2442529"},{"key":"22_CR2","doi-asserted-by":"crossref","unstructured":"Beyene, T.A., Chaudhuri, S., Popeea, C., Rybalchenko, A.: A constraint-based approach to solving games on infinite graphs. In: POPL (2014) (to appear)","DOI":"10.1145\/2535838.2535860"},{"key":"22_CR3","doi-asserted-by":"crossref","unstructured":"Bod\u00edk, R., Chandra, S., Galenson, J., Kimelman, D., Tung, N., Barman, S., Rodarmor, C.: Programming with angelic nondeterminism. In: POPL (2010)","DOI":"10.1145\/1706299.1706339"},{"key":"22_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/3-540-45657-0_7","volume-title":"Computer Aided Verification","author":"R.E. Bryant","year":"2002","unstructured":"Bryant, R.E., Lahiri, S.K., Seshia, S.A.: Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 78\u201392. Springer, Heidelberg (2002)"},{"key":"22_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/3-540-58179-0_44","volume-title":"Computer Aided Verification","author":"J.R. Burch","year":"1994","unstructured":"Burch, J.R., Dill, D.L.: Automatic verification of pipelined microprocessor control. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, pp. 68\u201380. Springer, Heidelberg (1994)"},{"key":"22_CR6","unstructured":"Celiku, O., von Wright, J.: Implementing angelic nondeterminism. In: Tenth Asia-Pacific Software Engineering Conference (2003)"},{"key":"22_CR7","doi-asserted-by":"crossref","unstructured":"Chaki, S., Clarke, E.M., Groce, A., Jha, S., Veith, H.: Modular verification of software components in c. In: ICSE, pp. 385\u2013395 (2003)","DOI":"10.1109\/ICSE.2003.1201217"},{"key":"22_CR8","doi-asserted-by":"crossref","unstructured":"Grumberg, O., Long, D.E.: Model checking and modular verification. ACM Transactions on Programming Languages and Systems\u00a016 (1991)","DOI":"10.1007\/3-540-54430-5_93"},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"Gulwani, S.: Automating string processing in spreadsheets using input-output examples. In: POPL (2011)","DOI":"10.1145\/1926385.1926423"},{"key":"22_CR10","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Harris, W.R., Singh, R.: Spreadsheet data manipulation using examples. CACM (2012)","DOI":"10.1145\/2240236.2240260"},{"key":"22_CR11","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Jha, S., Tiwari, A., Venkatesan, R.: Synthesis of loop-free programs. In: PLDI (2011)","DOI":"10.1145\/1993498.1993506"},{"key":"22_CR12","doi-asserted-by":"crossref","unstructured":"Itzhaky, S., Gulwani, S., Immerman, N., Sagiv, M.: A simple inductive synthesis methodology and its applications. In: OOPSLA (2010)","DOI":"10.1145\/1869459.1869463"},{"key":"22_CR13","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Complete functional synthesis. In: PLDI (2010)","DOI":"10.1145\/1806596.1806632"},{"key":"22_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"K.R.M. Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16. LNCS, vol.\u00a06355, pp. 348\u2013370. Springer, Heidelberg (2010)"},{"key":"22_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/978-3-642-00596-1_28","volume-title":"Foundations of Software Science and Computational Structures","author":"Y. Lustig","year":"2009","unstructured":"Lustig, Y., Vardi, M.Y.: Synthesis from component libraries. In: de Alfaro, L. (ed.) FOSSACS 2009. LNCS, vol.\u00a05504, pp. 395\u2013409. Springer, Heidelberg (2009)"},{"issue":"4","key":"22_CR16","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1109\/TSE.1979.234198","volume":"5","author":"Z. Manna","year":"1979","unstructured":"Manna, Z., Waldinger, R.: Synthesis: Dreams => program. IEEE Transactions on Software Engineering\u00a05(4), 294\u2013328 (1979)","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"1","key":"22_CR17","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1145\/357084.357090","volume":"2","author":"Z. Manna","year":"1980","unstructured":"Manna, Z., Waldinger, R.: A deductive approach to program synthesis. ACM Trans. Program. Lang. Syst.\u00a02(1), 90\u2013121 (1980)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"22_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/3-540-63166-6_6","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"1997","unstructured":"McMillan, K.L.: A compositional rule for hardware design refinement. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 24\u201335. Springer, Heidelberg (1997)"},{"key":"22_CR19","doi-asserted-by":"crossref","unstructured":"Seshia, S.A.: Sciduction: combining induction, deduction, and structure for verification and synthesis. In: DAC, pp. 356\u2013365 (2012)","DOI":"10.1145\/2228360.2228425"},{"key":"22_CR20","doi-asserted-by":"crossref","unstructured":"Singh, R., Gulwani, S.: Learning semantic string transformations from examples. PVLDB\u00a05 (2012)","DOI":"10.14778\/2212351.2212356"},{"key":"22_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"634","DOI":"10.1007\/978-3-642-31424-7_44","volume-title":"Computer Aided Verification","author":"R. Singh","year":"2012","unstructured":"Singh, R., Gulwani, S.: Synthesizing number transformations from input-output examples. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 634\u2013651. Springer, Heidelberg (2012)"},{"key":"22_CR22","doi-asserted-by":"crossref","unstructured":"Singh, R., Gulwani, S., Solar-Lezama, A.: Automated feedback generation for introductory programming assignments. In: PLDI (2013)","DOI":"10.1145\/2491956.2462195"},{"key":"22_CR23","doi-asserted-by":"crossref","unstructured":"Singh, R., Solar-Lezama, A.: Synthesizing data structure manipulations from storyboards. In: SIGSOFT FSE (2011)","DOI":"10.1145\/2025113.2025153"},{"key":"22_CR24","unstructured":"Solar-Lezama, A.: Program Synthesis By Sketching. PhD thesis, EECS Dept., UC Berkeley (2008)"},{"key":"22_CR25","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A.: Program sketching. STTT 15(5-6) (2013)","DOI":"10.1007\/s10009-012-0249-7"},{"key":"22_CR26","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Rabbah, R., Bodik, R., Ebcioglu, K.: Programming by sketching for bit-streaming programs. In: PLDI (2005)","DOI":"10.1145\/1065010.1065045"},{"key":"22_CR27","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Tancau, L., Bod\u00edk, R., Seshia, S.A., Saraswat, V.A.: Combinatorial sketching for finite programs. In: ASPLOS, pp. 404\u2013415 (2006)","DOI":"10.1145\/1168918.1168907"},{"key":"22_CR28","doi-asserted-by":"crossref","unstructured":"Srivastava, S., Gulwani, S., Chaudhuri, S., Foster, J.S.: Path-based inductive synthesis for program inversion. In: PLDI, pp. 492\u2013503 (2011)","DOI":"10.1145\/1993316.1993557"},{"key":"22_CR29","doi-asserted-by":"crossref","unstructured":"Srivastava, S., Gulwani, S., Foster, J.: From program verification to program synthesis. In: POPL (2010)","DOI":"10.1145\/1706299.1706337"},{"key":"22_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/3-540-16042-6_21","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"E.W. Stark","year":"1985","unstructured":"Stark, E.W.: A proof technique for rely\/guarantee properties. In: Maheshwari, S.N. (ed.) FSTTCS 1985. LNCS, vol.\u00a0206, pp. 369\u2013391. Springer, Heidelberg (1985)"},{"key":"22_CR31","doi-asserted-by":"crossref","unstructured":"Udupa, A., Raghavan, A., Deshmukh, J.V., Mador-Haim, S., Martin, M.M.K., Alur, R.: Transit: specifying protocols with concolic snippets. In: PLDI, pp. 287\u2013296 (2013)","DOI":"10.1145\/2499370.2462174"},{"key":"22_CR32","doi-asserted-by":"crossref","unstructured":"Vechev, M., Yahav, E., Yorsh, G.: Abstraction-guided synthesis of synchronization. In: POPL. ACM, New York (2010)","DOI":"10.1145\/1706299.1706338"},{"issue":"1","key":"22_CR33","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10703-012-0156-2","volume":"42","author":"C.M. Wintersteiger","year":"2013","unstructured":"Wintersteiger, C.M., Hamadi, Y., de Moura, L.M.: Efficiently solving quantified bit-vector formulas. Formal Methods in System Design\u00a042(1), 3\u201323 (2013)","journal-title":"Formal Methods in System Design"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-54013-4_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,25]],"date-time":"2019-05-25T19:42:40Z","timestamp":1558813360000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54013-4_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642540127","9783642540134"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54013-4_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}