{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:46:35Z","timestamp":1742913995651,"version":"3.40.3"},"publisher-location":"Cham","reference-count":54,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031223365"},{"type":"electronic","value":"9783031223372"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-22337-2_25","type":"book-chapter","created":{"date-parts":[[2022,12,28]],"date-time":"2022-12-28T10:08:41Z","timestamp":1672222121000},"page":"511-534","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Automated Program Repair Using Formal Verification Techniques"],"prefix":"10.1007","author":[{"given":"Hadar","family":"Frenkel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Orna","family":"Grumberg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bat-Chen","family":"Rothenberg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sarai","family":"Sheinvald","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,12,29]]},"reference":[{"key":"25_CR1","unstructured":"https:\/\/github.com\/hadarlh\/AGR"},{"key":"25_CR2","doi-asserted-by":"crossref","unstructured":"Albarghouthi, A., Dillig, I., Gurfinkel, A.: Maximal specification synthesis. In: POPL 51(1), 789-801(2016)","DOI":"10.1145\/2914770.2837628"},{"key":"25_CR3","doi-asserted-by":"crossref","unstructured":"Alpern, B., Wegman, M.N., Zadeck, F.K.: Detecting equality of variables in programs. In: POPL (1988)","DOI":"10.1145\/73560.73561"},{"issue":"2","key":"25_CR4","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0890-5401(87)90052-6","volume":"75","author":"D Angluin","year":"1987","unstructured":"Angluin, D.: Learning regular sets from queries and counterexamples. Inf. Comput. 75(2), 87\u2013106 (1987)","journal-title":"Inf. Comput."},{"key":"25_CR5","series-title":"Advances in Intelligent Systems and Computing","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-030-03405-4_17","volume-title":"Advances in Information and Communication Networks","author":"FY Assiri","year":"2019","unstructured":"Assiri, F.Y., Bieman, J.M.: MUT-APR: mutation-based automated program repair research tool. In: Arai, K., Kapoor, S., Bhatia, R. (eds.) FICC 2018. AISC, vol. 887, pp. 256\u2013270. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-03405-4_17"},{"key":"25_CR6","doi-asserted-by":"crossref","unstructured":"Attie, P.C., Dak, K., Bab, A.L., Sakr, M.: Model and program repair via SAT solving. ACM Trans. Embed. Comput. Syst. 17(2), 1\u201325 (2017)","DOI":"10.1145\/3147426"},{"key":"25_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-642-39611-3_24","volume-title":"Hardware and Software: Verification and Testing","author":"R Bloem","year":"2013","unstructured":"Bloem, R., Drechsler, R., Fey, G., Finder, A., Hofferek, G., K\u00f6nighofer, R., Raik, J., Repinski, U., S\u00fclflow, A.: FoREnSiC\u2013 an automatic debugging environment for C programs. In: Biere, A., Nahir, A., Vos, T. (eds.) HVC 2012. LNCS, vol. 7857, pp. 260\u2013265. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39611-3_24"},{"key":"25_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/978-3-540-71209-1_22","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Chaki","year":"2007","unstructured":"Chaki, S., Strichman, O.: Optimized L*-based assume-guarantee reasoning. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 276\u2013291. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71209-1_22"},{"key":"25_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1007\/978-3-642-14295-6_44","volume-title":"Computer Aided Verification","author":"Y-F Chen","year":"2010","unstructured":"Chen, Y.-F., Clarke, E.M., Farzan, A., Tsai, M.-H., Tsay, Y.-K., Wang, B.-Y.: Automated assume-guarantee reasoning through implicit learning. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 511\u2013526. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_44"},{"key":"25_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-3-642-00768-2_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y-F Chen","year":"2009","unstructured":"Chen, Y.-F., Farzan, A., Clarke, E.M., Tsay, Y.-K., Wang, B.-Y.: Learning minimal separating DFA\u2019s for compositional verification. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 31\u201345. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00768-2_3"},{"key":"25_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168\u2013176. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_15"},{"key":"25_CR12","doi-asserted-by":"crossref","unstructured":"Clarke, E., Kroening, D., Yorav, K.: Behavioral consistency of C and verilog programs using bounded model checking. In: Design Automation Conference, 2003. Proceedings, pp. 368\u2013371 IEEE (2003)","DOI":"10.21236\/ADA461052"},{"key":"25_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/3-540-36577-X_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"JM Cobleigh","year":"2003","unstructured":"Cobleigh, J.M., Giannakopoulou, D., P\u0103s\u0103reanu, C.S.: Learning assumptions for compositional verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 331\u2013346. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-36577-X_24"},{"key":"25_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-3-319-41540-6_21","volume-title":"Computer Aided Verification","author":"L D\u2019Antoni","year":"2016","unstructured":"D\u2019Antoni, L., Samanta, R., Singh, R.: Qlose: program repair with quantitative objectives. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 383\u2013401. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_21"},{"key":"25_CR15","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 de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"25_CR16","doi-asserted-by":"crossref","unstructured":"Debroy, V., Wong, W.E.: Using mutation to automatically suggest fixes for faulty programs. In: 2010 Third International Conference on Software Testing, Verification and Validation (ICST), pp. 65\u201374. IEEE (2010)","DOI":"10.1109\/ICST.2010.66"},{"key":"25_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"684","DOI":"10.1007\/978-3-642-39799-8_46","volume-title":"Computer Aided Verification","author":"I Dillig","year":"2013","unstructured":"Dillig, I., Dillig, T.: Explain: a tool for performing abductive inference. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 684\u2013689. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_46"},{"issue":"4","key":"25_CR18","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/s10664-005-3861-2","volume":"10","author":"H Do","year":"2005","unstructured":"Do, H., Elbaum, S., Rothermel, G.: Supporting controlled experimentation with testing techniques: an infrastructure and its potential impact. Empir. Softw. Eng. 10(4), 405\u2013435 (2005)","journal-title":"Empir. Softw. Eng."},{"key":"25_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-319-19249-9_3","volume-title":"FM 2015: Formal Methods","author":"KA Elkader","year":"2015","unstructured":"Elkader, K.A., Grumberg, O., P\u0103s\u0103reanu, C.S., Shoham, S.: Automated circular assume-guarantee reasoning. In: Bj\u00f8rner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 23\u201339. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-19249-9_3"},{"key":"25_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/978-3-319-41528-4_18","volume-title":"Computer Aided Verification","author":"K Abd Elkader","year":"2016","unstructured":"Abd Elkader, K., Grumberg, O., P\u0103s\u0103reanu, C.S., Shoham, S.: Automated circular assume-guarantee reasoning with N-way decomposition and alphabet refinement. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 329\u2013351. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_18"},{"key":"25_CR21","unstructured":"Frenkel, H.: Automata over infinite data domains: learnability and applications in program verification and repair, Ph. D thesis (2021)"},{"key":"25_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/978-3-030-45190-5_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Frenkel","year":"2020","unstructured":"Frenkel, H., Grumberg, O., P\u0103s\u0103reanu, C., Sheinvald, S.: Assume, guarantee or repair. In: TACAS 2020. LNCS, vol. 12078, pp. 211\u2013227. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_12"},{"key":"25_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/978-3-540-71209-1_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Gheorghiu","year":"2007","unstructured":"Gheorghiu, M., Giannakopoulou, D., P\u0103s\u0103reanu, C.S.: Refining interface alphabets for compositional verification. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 292\u2013307. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71209-1_23"},{"key":"25_CR24","doi-asserted-by":"crossref","unstructured":"Giannakopoulou, D., P\u0103s\u0103reanu, C.S., Barringer, H.: Assumption Generation for Software Component Verification. In: IEEE Computer Society. ASE (2002)","DOI":"10.1109\/ASE.2002.1114984"},{"issue":"3","key":"25_CR25","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/s10515-005-2641-y","volume":"12","author":"D Giannakopoulou","year":"2005","unstructured":"Giannakopoulou, D., P\u0103s\u0103reanu, C.S., Barringer, H.: Component verification with automatically generated assumptions. Autom. Softw. Eng. 12(3), 297\u2013320 (2005)","journal-title":"Autom. Softw. Eng."},{"issue":"3","key":"25_CR26","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/s10703-008-0050-0","volume":"32","author":"A Gupta","year":"2008","unstructured":"Gupta, A., McMillan, K.L., Fu, Z.: Automated assumption generation for compositional verification. Formal Methods Syst. Des. 32(3), 285\u2013301 (2008)","journal-title":"Formal Methods Syst. Des."},{"key":"25_CR27","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). https:\/\/doi.org\/10.1007\/11513988_23"},{"key":"25_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/978-3-319-21668-3_13","volume-title":"Computer Aided Verification","author":"E Kneuss","year":"2015","unstructured":"Kneuss, E., Koukoutos, M., Kuncak, V.: Deductive program repair. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 217\u2013233. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21668-3_13"},{"key":"25_CR29","unstructured":"K\u00f6nighofer, R., Bloem, R.: Automated error localization and correction for imperative programs. In: Formal Methods in Computer-Aided Design (FMCAD), pp. 91\u2013100. IEEE (2011)"},{"key":"25_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1007\/978-3-642-39611-3_11","volume-title":"Hardware and Software: Verification and Testing","author":"R K\u00f6nighofer","year":"2013","unstructured":"K\u00f6nighofer, R., Bloem, R.: Repair with on-the-fly program analysis. In: Biere, A., Nahir, A., Vos, T. (eds.) HVC 2012. LNCS, vol. 7857, pp. 56\u201371. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39611-3_11"},{"issue":"1","key":"25_CR31","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1109\/TSE.2011.104","volume":"38","author":"C Le Goues","year":"2012","unstructured":"Le Goues, C., Nguyen, T., Forrest, S., Weimer, W.: GenProg: a generic method for automatic software repair. Softw. Eng. IEEE Trans. 38(1), 54\u201372 (2012)","journal-title":"Softw. Eng. IEEE Trans."},{"key":"25_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1007\/978-3-642-36742-7_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B Li","year":"2013","unstructured":"Li, B., Dillig, I., Dillig, T., McMillan, K., Sagiv, M.: Synthesis of circular compositional program proofs via abduction. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 370\u2013384. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_26"},{"key":"25_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"416","DOI":"10.1007\/978-3-319-06410-9_29","volume-title":"FM 2014: Formal Methods","author":"S-W Lin","year":"2014","unstructured":"Lin, S.-W., Hsiung, P.-A.: Compositional synthesis of concurrent systems through causal model checking and learning. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 416\u2013431. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-06410-9_29"},{"key":"25_CR34","doi-asserted-by":"crossref","unstructured":"Liu, K., Koyuncu, A., Bissyande, T.F., Kim, D., Klein, J., Le Traon, Y.: You cannot fix what you cannot find! an investigation of fault localization bias in benchmarking automated program repair systems. In: ICST, pp. 102\u2013113 (2019)","DOI":"10.1109\/ICST.2019.00020"},{"key":"25_CR35","unstructured":"Magee, J., Kramer, J.: Concurrency - State Models and Java Programs. Wiley (1999)"},{"key":"25_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/3-540-48153-2_30","volume-title":"Correct Hardware Design and Verification Methods","author":"KL McMillan","year":"1999","unstructured":"McMillan, K.L.: Circular compositional reasoning about liveness. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 342\u2013346. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48153-2_30"},{"key":"25_CR37","doi-asserted-by":"crossref","unstructured":"Mechtaev, S., Nguyen, M.-D., Noller, Y., Grunske, L., Roychoudhury, A.: Semantic program repair using a reference implementation. In: ICSE, pp. 129\u2013139 (2018)","DOI":"10.1145\/3180155.3180247"},{"key":"25_CR38","doi-asserted-by":"crossref","unstructured":"Mechtaev, S., Yi, J., Roychoudhury, A.: Angelix: scalable multiline program patch synthesis via symbolic analysis. In: ICSE, ICSE (2016)","DOI":"10.1145\/2884781.2884807"},{"issue":"4","key":"25_CR39","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1109\/TSE.1981.230844","volume":"7","author":"J Misra","year":"1981","unstructured":"Misra, J., Chandy, K.M.: Proofs of networks of processes. IEEE Trans. Software Eng. 7(4), 417\u2013426 (1981)","journal-title":"IEEE Trans. Software Eng."},{"key":"25_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/10722167_14","volume-title":"Computer Aided Verification","author":"KS Namjoshi","year":"2000","unstructured":"Namjoshi, K.S., Trefler, R.J.: On the completeness of compositional reasoning. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 139\u2013153. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722167_14"},{"key":"25_CR41","doi-asserted-by":"crossref","unstructured":"Nguyen, H.D.T., Qi, D., Roychoudhury, A., Chandra, S.: SemFix: program repair via semantic analysis. In: Proceedings of the 2013 International Conference on Software Engineering, pp. 772\u2013781. IEEE Press (2013)","DOI":"10.1109\/ICSE.2013.6606623"},{"key":"25_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/978-3-662-54577-5_17","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"TV Nguyen","year":"2017","unstructured":"Nguyen, T.V., Weimer, W., Kapur, D., Forrest, S.: Connecting Program Synthesis and Reachability: Automatic Program Repair Using Test-Input Generation. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 301\u2013318. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_17"},{"key":"25_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-030-11245-5_4","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T-T Nguyen","year":"2019","unstructured":"Nguyen, T.-T., Ta, Q.-T., Chin, W.-N.: Automatic program repair using formal verification and expression templates. In: Enea, C., Piskac, R. (eds.) VMCAI 2019. LNCS, vol. 11388, pp. 70\u201391. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-11245-5_4"},{"key":"25_CR44","doi-asserted-by":"publisher","unstructured":"P\u0103s\u0103reanu, C.S., Giannakopoulou, D., Bobaru, M.G., Cobleigh, J.M., Barringer, H.: Learning to divide and conquer: applying the L* algorithm to automate assume-guarantee reasoning. Form. Methods Syst. Des. 32, 175\u2013205 (2008). https:\/\/doi.org\/10.1007\/s10703-008-0049-6","DOI":"10.1007\/s10703-008-0049-6"},{"key":"25_CR45","unstructured":"Peirce, C., Hartshorne, C.: Collected papers of charles sanders peirce. Belknap Press (1932)"},{"key":"25_CR46","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: In transition from global to modular temporal reasoning about programs. In: Logics and Models of Concurrent Systems, NATO ASI Series (1985)","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"25_CR47","doi-asserted-by":"crossref","unstructured":"Repinski, U., Hantson, H., Jenihhin, M., Raik, J., Ubar, R., Guglielmo, G.D., Pravadelli, G., Fummi, F.: Combining dynamic slicing and mutation operators for ESL correction. In: Test Symposium (ETS), 2012 17th IEEE European, pp. 1\u20136. IEEE (2012)","DOI":"10.1109\/ETS.2012.6233020"},{"key":"25_CR48","unstructured":"Rothenberg, B.-C.: Formal automated program repair, Ph. D. thesis (2020)"},{"key":"25_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"593","DOI":"10.1007\/978-3-319-48989-6_36","volume-title":"FM 2016: Formal Methods","author":"B-C Rothenberg","year":"2016","unstructured":"Rothenberg, B.-C., Grumberg, O.: Sound and complete mutation-based program repair. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 593\u2013611. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-48989-6_36"},{"key":"25_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"658","DOI":"10.1007\/978-3-030-53291-8_33","volume-title":"Computer Aided Verification","author":"B-C Rothenberg","year":"2020","unstructured":"Rothenberg, B.-C., Grumberg, O.: Must fault localization for program repair. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 658\u2013680. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_33"},{"key":"25_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1007\/978-3-642-14295-6_45","volume-title":"Computer Aided Verification","author":"R Singh","year":"2010","unstructured":"Singh, R., Giannakopoulou, D., P\u0103s\u0103reanu, C.: Learning component interfaces with may and must abstractions. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 527\u2013542. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_45"},{"key":"25_CR52","unstructured":"Tan, S. H., Yi, J., Yulis, Mechtaev, S., Roychoudhury, A.: Codeflaws: a programming competition benchmark for evaluating automated program repair tools. In: Proceedings - 2017 IEEE\/ACM 39th International Conference on Software Engineering Companion, ICSE-C 2017, pp. 180\u2013182 (2017)"},{"issue":"1","key":"25_CR53","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1007\/s10703-015-0223-6","volume":"47","author":"C von Essen","year":"2015","unstructured":"von Essen, C., Jobstmann, B.: Program repair without regret. Formal Methods Syst. Des. 47(1), 26\u201350 (2015). https:\/\/doi.org\/10.1007\/s10703-015-0223-6","journal-title":"Formal Methods Syst. Des."},{"key":"25_CR54","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/BFb0099397","volume-title":"Models and Sets","author":"V Weispfenning","year":"1984","unstructured":"Weispfenning, V.: Quantifier elimination and decision procedures for valued fields. In: M\u00fcller, G.H., Richter, M.M. (eds.) Models and Sets. LNM, vol. 1103, pp. 419\u2013472. Springer, Heidelberg (1984). https:\/\/doi.org\/10.1007\/BFb0099397"}],"container-title":["Lecture Notes in Computer Science","Principles of Systems Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-22337-2_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,11]],"date-time":"2024-10-11T02:55:53Z","timestamp":1728615353000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-22337-2_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031223365","9783031223372"],"references-count":54,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-22337-2_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"29 December 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}