{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T03:09:20Z","timestamp":1743044960862,"version":"3.40.3"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319296128"},{"type":"electronic","value":"9783319296135"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-29613-5_2","type":"book-chapter","created":{"date-parts":[[2016,1,28]],"date-time":"2016-01-28T02:47:34Z","timestamp":1453949254000},"page":"19-39","source":"Crossref","is-referenced-by-count":1,"title":["Recursive Games for Compositional Program Synthesis"],"prefix":"10.1007","author":[{"given":"Tewodros A.","family":"Beyene","sequence":"first","affiliation":[]},{"given":"Swarat","family":"Chaudhuri","sequence":"additional","affiliation":[]},{"given":"Corneliu","family":"Popeea","sequence":"additional","affiliation":[]},{"given":"Andrey","family":"Rybalchenko","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Albarghouthi, A., Li, Y., Gurfinkel, A., Chechik, M.: UFO: a framework for abstraction- and interpolation-based software verification. In: CAV (2012)","DOI":"10.1007\/978-3-642-31424-7_48"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/978-3-642-11319-2_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R Alur","year":"2010","unstructured":"Alur, R., Chaudhuri, S.: Temporal reasoning for procedural programs. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 45\u201360. Springer, Heidelberg (2010)"},{"issue":"1","key":"2_CR3","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1145\/1111320.1111051","volume":"41","author":"Rajeev Alur","year":"2006","unstructured":"Alur, R., Chaudhuri, S., Madhusudan, P.: A fixpoint calculus for local and global program flows. In: POPL, pp. 153\u2013165 (2006)","journal-title":"ACM SIGPLAN Notices"},{"key":"2_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/11817963_31","volume-title":"Computer Aided Verification","author":"R Alur","year":"2006","unstructured":"Alur, R., Chaudhuri, S., Madhusudan, P.: Languages of nested trees. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 329\u2013342. Springer, Heidelberg (2006)"},{"issue":"5","key":"2_CR5","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1145\/2039346.2039347","volume":"33","author":"R Alur","year":"2011","unstructured":"Alur, R., Chaudhuri, S., Madhusudan, P.: Software model checking using languages of nested trees. ACM Trans. Program. Lang. Syst. 33(5), 15 (2011)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"1","key":"2_CR6","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/565816.503274","volume":"37","author":"Thomas Ball","year":"2002","unstructured":"Ball, T., Rajamani, S.K.: The SLAM project: debugging system software via static analysis. In: POPL (2002)","journal-title":"ACM SIGPLAN Notices"},{"key":"2_CR7","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)","DOI":"10.1145\/2535838.2535860"},{"key":"2_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"869","DOI":"10.1007\/978-3-642-39799-8_61","volume-title":"Computer Aided Verification","author":"TA Beyene","year":"2013","unstructured":"Beyene, T.A., Popeea, C., Rybalchenko, A.: Solving existentially quantified horn clauses. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 869\u2013882. Springer, Heidelberg (2013)"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"594","DOI":"10.1007\/978-3-642-36742-7_43","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Beyer","year":"2013","unstructured":"Beyer, D.: Second competition on software verification. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 594\u2013609. Springer, Heidelberg (2013)"},{"key":"2_CR10","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1007\/978-3-642-22110-1_16","volume-title":"Computer Aided Verification","author":"Dirk Beyer","year":"2011","unstructured":"Beyer, D., Keremoglu, M.E.: CPACHECKER: a tool for configurable software verification. In: CAV (2011)"},{"key":"2_CR11","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1090\/S0002-9947-1969-0280205-0","volume":"138","author":"JR B\u00fcchi","year":"1969","unstructured":"B\u00fcchi, J.R., Landweber, L.: Solving sequential conditions by finite-state strategies. Trans. Amer. Math. Soc. 138, 295\u2013311 (1969)","journal-title":"Trans. Amer. Math. Soc."},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"704","DOI":"10.1007\/3-540-45465-9_60","volume-title":"Automata, Languages and Programming","author":"T Cachat","year":"2002","unstructured":"Cachat, T.: Symbolic strategy synthesis for games on pushdown graphs. In: Widmayer, P., Triguero, F., Morales, R., Hennessy, M., Eidenbenz, S., Conejo, R. (eds.) ICALP 2002. LNCS, vol. 2380, pp. 704\u2013715. Springer, Heidelberg (2002)"},{"issue":"3","key":"2_CR13","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/s10703-009-0087-8","volume":"35","author":"B Cook","year":"2009","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Summarization for termination: no return!. Formal Methods Syst. Design 35(3), 369\u2013387 (2009)","journal-title":"Formal Methods Syst. Design"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"2_CR15","series-title":"Lecture Notes in Computer Science","volume-title":"Automata, Logics, and Infinite Games","year":"2002","unstructured":"Gr\u00e4del, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games. LNCS, vol. 2500. Springer, Heidelberg (2002)"},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: PLDI (2012)","DOI":"10.1145\/2254064.2254112"},{"key":"2_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1007\/11817963_33","volume-title":"Computer Aided Verification","author":"A Griesmayer","year":"2006","unstructured":"Griesmayer, A., Bloem, R., Cook, B.: Repair of boolean programs with an application to C. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 358\u2013371. Springer, Heidelberg (2006)"},{"key":"2_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-540-30579-8_16","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"O Grumberg","year":"2005","unstructured":"Grumberg, O., Lange, M., Leucker, M., Shoham, S.: Don\u2019t Know in the \n                    \n                      \n                    \n                    $$\\mu $$\n                    \n                      \n                        \u03bc\n                      \n                    \n                  -Calculus. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 233\u2013249. Springer, Heidelberg (2005)"},{"key":"2_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/11691372_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Gurfinkel","year":"2006","unstructured":"Gurfinkel, A., Chechik, M.: Why waste a perfectly good abstraction? In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 212\u2013226. Springer, Heidelberg (2006)"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL (2004)","DOI":"10.1145\/964001.964021"},{"key":"2_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"457","DOI":"10.1007\/978-3-642-22110-1_36","volume-title":"Computer Aided Verification","author":"K Hoder","year":"2011","unstructured":"Hoder, K., Bj\u00f8rner, N., de Moura, L.: \n                    \n                      \n                    \n                    $$\\mu $$\n                    \n                      \n                        \u03bc\n                      \n                    \n                  Z\u2013 an efficient engine for fixed points with constraints. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 457\u2013462. Springer, Heidelberg (2011)"},{"key":"2_CR22","unstructured":"Holzbaur, C.: OFAI clp(q, r) Manual, 1.3.3(edn.). Austrian Research Institute for Artificial Intelligence, Vienna, TR-95-09 (1995)"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"Jha, S., Gulwani, S., Seshia, S.A., Tiwari, A.: Oracle-guided component-based program synthesis. In: ICSE (2010)","DOI":"10.1145\/1806799.1806833"},{"key":"2_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/11513988_23","volume-title":"Computer Aided Verification","author":"B Jobstmann","year":"2005","unstructured":"Jobstmann, B., Griesmayer, A., Bloem, R.: Program repair as a game. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 226\u2013238. Springer, Heidelberg (2005)"},{"key":"2_CR25","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Complete functional synthesis. In: PLDI (2010)","DOI":"10.1145\/1806596.1806632"},{"issue":"5\u20136","key":"2_CR26","doi-asserted-by":"publisher","first-page":"603","DOI":"10.1007\/s10009-012-0236-z","volume":"15","author":"Y Lustig","year":"2013","unstructured":"Lustig, Y., Vardi, M.Y.: Synthesis from component libraries. STTT 15(5\u20136), 603\u2013618 (2013)","journal-title":"STTT"},{"key":"2_CR27","unstructured":"Madhusudan, P.: Synthesizing reactive programs. In: CSL, pp. 428\u2013442 (2011)"},{"key":"2_CR28","first-page":"213","volume-title":"Lecture Notes in Computer Science","author":"George C. Necula","year":"2002","unstructured":"Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: CIL: Intermediate language and tools for analysis and transformation of C programs. In: CC (2002)"},{"key":"2_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11609773_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"N Piterman","year":"2006","unstructured":"Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive(1) designs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 364\u2013380. Springer, Heidelberg (2006)"},{"key":"2_CR30","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL, pp. 179\u2013190. ACM (1989)","DOI":"10.1145\/75277.75293"},{"key":"2_CR31","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS (2004)","DOI":"10.1109\/LICS.2004.1319598"},{"key":"2_CR32","unstructured":"Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. In: Program Flow Analysis: Theory and Applications, pp. 189\u2013234 (1981)"},{"key":"2_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/978-3-642-54013-4_22","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R Singh","year":"2014","unstructured":"Singh, R., Singh, R., Xu, Z., Krosnick, R., Solar-Lezama, A.: Modular synthesis of sketches using models. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 395\u2013414. Springer, Heidelberg (2014)"},{"issue":"11","key":"2_CR34","doi-asserted-by":"crossref","first-page":"404","DOI":"10.1145\/1168918.1168907","volume":"41","author":"Armando Solar-Lezama","year":"2006","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)","journal-title":"ACM SIGPLAN Notices"},{"key":"2_CR35","doi-asserted-by":"crossref","unstructured":"Srivastava, S., Gulwani, S., Foster, J.S.: From program verification to program synthesis. In: POPL, pp. 313\u2013326 (2010)","DOI":"10.1145\/1707801.1706337"},{"key":"2_CR36","first-page":"1","volume-title":"STACS 95","author":"Wolfgang Thomas","year":"1995","unstructured":"Thomas, W.: On the synthesis of strategies in infinite games. In: STACS, pp. 1\u201313 (1995)"},{"issue":"1","key":"2_CR37","doi-asserted-by":"crossref","first-page":"327","DOI":"10.1145\/1707801.1706338","volume":"45","author":"Martin Vechev","year":"2010","unstructured":"Vechev, M.T., Yahav, E., Yorsh, G.: Abstraction-guided synthesis of synchronization. In: POPL (2010)","journal-title":"ACM SIGPLAN Notices"},{"issue":"2","key":"2_CR38","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1006\/inco.2000.2894","volume":"164","author":"I Walukiewicz","year":"2001","unstructured":"Walukiewicz, I.: Pushdown processes: games and model-checking. Inf. Comput. 164(2), 234\u2013263 (2001)","journal-title":"Inf. Comput."},{"issue":"3","key":"2_CR39","doi-asserted-by":"crossref","first-page":"16","DOI":"10.1145\/1232420.1232423","volume":"29","author":"Yichen Xie","year":"2007","unstructured":"Xie, Y., Aiken, A.: SATURN: A scalable framework for error detection using boolean satisfiability. ACM TOPLAS, 29(3) (2007)","journal-title":"ACM Transactions on Programming Languages and Systems"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, and Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-29613-5_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T07:49:48Z","timestamp":1559375388000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-29613-5_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319296128","9783319296135"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-29613-5_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}