{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T08:14:46Z","timestamp":1770279286693,"version":"3.49.0"},"publisher-location":"Cham","reference-count":27,"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_13","type":"book-chapter","created":{"date-parts":[[2015,7,13]],"date-time":"2015-07-13T15:08:53Z","timestamp":1436800133000},"page":"217-233","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":32,"title":["Deductive Program Repair"],"prefix":"10.1007","author":[{"given":"Etienne","family":"Kneuss","sequence":"first","affiliation":[]},{"given":"Manos","family":"Koukoutos","sequence":"additional","affiliation":[]},{"given":"Viktor","family":"Kuncak","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,14]]},"reference":[{"key":"13_CR1","unstructured":"Alur, R., Bodik, R., Dallal, E., Fisman, D., Garg, P., Juniwal, G., Kress-Gazit, H., Madhusudan, P., Martin, M.M.K., Raghothaman, M., Saha, S., Seshia, S. A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-guided synthesis. To Appear in Marktoberdrof NATO proceedings, (2014). http:\/\/sygus.seas.upenn.edu\/files\/sygus_extended.pdf . Accessed 02 June 2015"},{"key":"13_CR2","doi-asserted-by":"crossref","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: FMCAD, pp. 1\u201317. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"13_CR3","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1145\/1985793.1985811","volume-title":"ICSE","author":"S Chandra","year":"2011","unstructured":"Chandra, S., Torlak, E., Barman, S., Bod\u00edk, R.: Angelic debugging. In: Taylor, R.N., Gall, H.C., Medvidovic, N. (eds.) ICSE, pp. 121\u2013130. ACM, New york (2011)"},{"key":"13_CR4","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":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"10","DOI":"10.1007\/978-3-642-18070-5_2","volume-title":"Formal Verification of Object-Oriented Software","author":"M F\u00e4hndrich","year":"2011","unstructured":"F\u00e4hndrich, M., Logozzo, F.: Static contract checking with abstract interpretation. In: Beckert, B., March\u00e9, C. (eds.) FoVeOOS 2010. LNCS, vol. 6528, pp. 10\u201330. Springer, Heidelberg (2011)"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-642-19835-9_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Gopinath","year":"2011","unstructured":"Gopinath, D., Malik, M.Z., Khurshid, S.: Specification-Based Program Repair Using SAT. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 173\u2013188. Springer, Heidelberg (2011)"},{"issue":"1","key":"13_CR7","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1109\/TSE.2011.104","volume":"38","author":"CL Goues","year":"2012","unstructured":"Goues, C.L., Nguyen, T., Forrest, S., Weimer, W.: Genprog: a generic method for automatic software repair. TSE 38(1), 54\u201372 (2012)","journal-title":"TSE"},{"key":"13_CR8","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":"13_CR9","doi-asserted-by":"crossref","unstructured":"Gvero, T., Kuncak, V., Kuraj, I., Piskac, R., Complete completion using types and weights. In: PLDI, pp. 27\u201338 (2013)","DOI":"10.1145\/2499370.2462192"},{"key":"13_CR10","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)"},{"issue":"2","key":"13_CR11","first-page":"441","volume":"78","author":"B Jobstmann","year":"2012","unstructured":"Jobstmann, B., Staber, S., Griesmayer, A., Bloem, R.: Finding and fixing faults. JCSS 78(2), 441\u2013460 (2012)","journal-title":"JCSS"},{"key":"13_CR12","first-page":"437","volume-title":"PLDI","author":"M Jose","year":"2011","unstructured":"Jose, M., Majumdar, R.: Cause clue clauses: error localization using maximum satisfiability. In: Hall, M.W., Padua, D.A. (eds.) PLDI, pp. 437\u2013446. ACM, New york (2011)"},{"key":"13_CR13","first-page":"407","volume-title":"OOPSLA","author":"E Kneuss","year":"2013","unstructured":"Kneuss, E., Kuraj, I., Kuncak, V., Suter, P.: Synthesis modulo recursive functions. In: Hosking, A.L., Eugster, P.T., Lopes, C.V. (eds.) OOPSLA, pp. 407\u2013426. ACM, New york (2013)"},{"key":"13_CR14","first-page":"91","volume-title":"FMCAD","author":"R K\u00f6nighofer","year":"2011","unstructured":"K\u00f6nighofer, R., Bloem, R.: Automated error localization and correction for imperative programs. In: Bjesse, P., Slobodov\u00e1, A. (eds.) FMCAD, pp. 91\u2013100. FMCAD Inc, Austin (2011)"},{"issue":"5\u20136","key":"13_CR15","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1007\/s10009-011-0217-7","volume":"15","author":"V Kuncak","year":"2013","unstructured":"Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Functional synthesis for linear arithmetic and sets. STTT 15(5\u20136), 455\u2013474 (2013)","journal-title":"STTT"},{"key":"13_CR16","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1145\/2384616.2384626","volume-title":"OOPSLA","author":"F Logozzo","year":"2012","unstructured":"Logozzo, F., Ball, T.: Modular and verified automatic program repair. In: Leavens, G.T., Dwyer, M.B. (eds.) OOPSLA, pp. 133\u2013146. ACM, Newyork (2012)"},{"key":"13_CR17","first-page":"772","volume-title":"ICSE","author":"HDT Nguyen","year":"2013","unstructured":"Nguyen, H.D.T., Qi, D., Roychoudhury, A., Chandra, S.: Semfix: program repair via semantic analysis. In: Notkin, D., Cheng, B.H.C., Pohl, K. (eds.) ICSE, pp. 772\u2013781. IEEE and ACM, New York (2013)"},{"key":"13_CR18","unstructured":"Pei, Y., Wei, Y., Furia, C.A., Nordio, M., Meyer, B.: Code-based automated program fixing. ArXiv e-prints (2011). arXiv:1102.1059"},{"key":"13_CR19","first-page":"1","volume-title":"FMCAD","author":"R Samanta","year":"2008","unstructured":"Samanta, R., Deshmukh, J.V., Emerson, E.A.: Automatic generation of local repairs for boolean programs. In: Cimatti, A., Jones, R.B. (eds.) FMCAD, pp. 1\u201310. IEEE, New York (2008)"},{"key":"13_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"268","DOI":"10.1007\/978-3-319-10936-7_17","volume-title":"Static Analysis","author":"R Samanta","year":"2014","unstructured":"Samanta, R., Olivo, O., Emerson, E.A.: Cost-aware automatic program repair. In: M\u00fcller-Olm, M., Seidl, H. (eds.) Static Analysis. LNCS, vol. 8723, pp. 268\u2013284. Springer, Heidelberg (2014)"},{"issue":"5\u20136","key":"13_CR21","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. STTT 15(5\u20136), 475\u2013495 (2013)","journal-title":"STTT"},{"key":"13_CR22","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"},{"issue":"5\u20136","key":"13_CR23","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1007\/s10009-012-0223-4","volume":"15","author":"S Srivastava","year":"2013","unstructured":"Srivastava, S., Gulwani, S., Foster, J.S.: Template-based program verification and program synthesis. STTT 15(5\u20136), 497\u2013518 (2013)","journal-title":"STTT"},{"key":"13_CR24","unstructured":"Suter, P.: Programming with Specifications. Ph.D. thesis, EPFL, December 2012"},{"key":"13_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-642-23702-7_23","volume-title":"Static Analysis","author":"P Suter","year":"2011","unstructured":"Suter, P., K\u00f6ksal, A.S., Kuncak, V.: Satisfiability modulo recursive programs. In: Yahav, E. (ed.) Static Analysis. LNCS, vol. 6887, pp. 298\u2013315. Springer, Heidelberg (2011)"},{"key":"13_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"896","DOI":"10.1007\/978-3-642-39799-8_64","volume-title":"Computer Aided Verification","author":"C Essen von","year":"2013","unstructured":"von Essen, C., Jobstmann, B.: Program repair without regret. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 896\u2013911. Springer, Heidelberg (2013)"},{"issue":"2","key":"13_CR27","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1109\/32.988498","volume":"28","author":"A Zeller","year":"2002","unstructured":"Zeller, A., Hildebrandt, R.: Simplifying and isolating failure-inducing input. TSE 28(2), 183\u2013200 (2002)","journal-title":"TSE"}],"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_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,18]],"date-time":"2022-05-18T00:51:11Z","timestamp":1652835071000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-21668-3_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319216676","9783319216683"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21668-3_13","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"}}]}}