{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,15]],"date-time":"2026-08-15T16:16:34Z","timestamp":1786810594663,"version":"build-2736575974"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030112448","type":"print"},{"value":"9783030112455","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"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":[[2019]]},"DOI":"10.1007\/978-3-030-11245-5_4","type":"book-chapter","created":{"date-parts":[[2019,1,10]],"date-time":"2019-01-10T13:45:18Z","timestamp":1547127918000},"page":"70-91","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":22,"title":["Automatic Program Repair Using Formal Verification and Expression Templates"],"prefix":"10.1007","author":[{"given":"Thanh-Toan","family":"Nguyen","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Quang-Trung","family":"Ta","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Wei-Ngan","family":"Chin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,1,11]]},"reference":[{"issue":"9","key":"4_CR1","doi-asserted-by":"publisher","first-page":"1006","DOI":"10.1016\/j.scico.2010.07.004","volume":"77","author":"W-N Chin","year":"2012","unstructured":"Chin, W.-N., David, C., Nguyen, H.H., Qin, S.: Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Sci. Comput. Program. (SCP) 77(9), 1006\u20131036 (2012)","journal-title":"Sci. Comput. Program. (SCP)"},{"key":"4_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/978-3-540-45069-6_39","volume-title":"Computer Aided Verification","author":"MA Col\u00f3n","year":"2003","unstructured":"Col\u00f3n, M.A., Sankaranarayanan, S., Sipma, H.B.: Linear invariant generation using non-linear constraint solving. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 420\u2013432. Springer, Heidelberg (2003). \nhttps:\/\/doi.org\/10.1007\/978-3-540-45069-6_39"},{"issue":"4","key":"4_CR3","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.G., Rothermel, G.: Supporting controlled experimentation with testing techniques: an infrastructure and its potential impact. Empirical Softw. Eng. 10(4), 405\u2013435 (2005)","journal-title":"Empirical Softw. Eng."},{"issue":"10","key":"4_CR4","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"4_CR5","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511810275","volume-title":"Logic in Computer Science: Modelling and Reasoning About Systems","author":"M Huth","year":"2004","unstructured":"Huth, M., Ryan, M.: Logic in Computer Science: Modelling and Reasoning About Systems. Cambridge University Press, New York (2004). ISBN 052154310X"},{"key":"4_CR6","unstructured":"ISO. ISO\/IEC 9899: 2011 information technology - programming languages - C. Int. Organ. Stand. 27, 59 (2011)"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Jones, J.A., Harrold, M.J., Stasko, J.T.: Visualization of test information to assist fault localization. In: International Conference on Software Engineering (ICSE), pp. 467\u2013477 (2002)","DOI":"10.1145\/581396.581397"},{"key":"4_CR8","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). \nhttps:\/\/doi.org\/10.1007\/978-3-319-21668-3_13"},{"key":"4_CR9","unstructured":"K\u00f6nighofer, R., Bloem, R.: Automated error localization and correction for imperative programs. In: International Conference on Formal Methods in Computer-Aided Design (FMCAD), pp. 91\u2013100 (2011)"},{"key":"4_CR10","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). \nhttps:\/\/doi.org\/10.1007\/978-3-642-39611-3_11"},{"issue":"1","key":"4_CR11","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1109\/TSE.2011.104","volume":"38","author":"C Goues Le","year":"2012","unstructured":"Le Goues, C., Nguyen, T., Forrest, S., Weimer, W.: GenProg: a generic method for automatic software repair. IEEE Trans. Softw. Eng. 38(1), 54\u201372 (2012)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","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":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). \nhttps:\/\/doi.org\/10.1007\/978-3-642-17511-4_20"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"Logozzo, F., Ball, T.: Modular and verified automatic program repair. In: International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA), pp. 133\u2013146 (2012)","DOI":"10.1145\/2384616.2384626"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Long, F., Rinard, M.: Staged program repair with condition synthesis. In: Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC\/FSE), pp. 166\u2013178 (2015)","DOI":"10.1145\/2786805.2786811"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Mechtaev, S., Yi, J., Roychoudhury, A.: Angelix: scalable multiline program patch synthesis via symbolic analysis. In: International Conference on Software Engineering (ICSE), pp. 691\u2013701 (2016)","DOI":"10.1145\/2884781.2884807"},{"key":"4_CR16","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.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"Nguyen, H.D.T., Qi, D., Roychoudhury, A., Chandra, S.: SemFix: program repair via semantic analysis. In: International Conference on Software Engineering (ICSE), pp. 772\u2013781 (2013)","DOI":"10.1109\/ICSE.2013.6606623"},{"issue":"5","key":"4_CR18","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1109\/TSE.2014.2312918","volume":"40","author":"Y Pei","year":"2014","unstructured":"Pei, Y., Furia, C.A., Nordio, M., Wei, Y., Meyer, B., Zeller, A.: Automated fixing of programs with contracts. IEEE Trans. Softw. Eng. 40(5), 427\u2013449 (2014)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"4_CR19","unstructured":"Program Repair Website (2018). \nhttp:\/\/program-repair.org\/\n\n. Accessed 18 Sept 2018"},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"Qi, Y., Mao, X., Lei, Y., Dai, Z., Wang, C.: The strength of random search on automated program repair. In: International Conference on Software Engineering (ICSE), pp. 254\u2013265 (2014)","DOI":"10.1145\/2568225.2568254"},{"key":"4_CR21","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). \nhttps:\/\/doi.org\/10.1007\/978-3-319-48989-6_36"},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"Smith, E.K., Barr, E.T., Le Goues, C., Brun, Y.: Is the cure worse than the disease? Overfitting in automated program repair. In: Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC\/FSE), pp. 532\u2013543 (2015)","DOI":"10.1145\/2786805.2786825"},{"issue":"POPL","key":"4_CR23","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3158097","volume":"2","author":"Quang-Trung Ta","year":"2017","unstructured":"Ta, Q.-T., Le, T.C., Khoo, S.C., Chin, W.N.: Automated lemma synthesis in symbolic-heap separation logic. In: Symposium on Principles of Programming Languages (POPL), pp. 9:1\u20139:29 (2018)","journal-title":"Proceedings of the ACM on Programming Languages"},{"key":"4_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"659","DOI":"10.1007\/978-3-319-48989-6_40","volume-title":"FM 2016: Formal Methods","author":"Q-T Ta","year":"2016","unstructured":"Ta, Q.-T., Le, T.C., Khoo, S.-C., Chin, W.-N.: Automated mutual explicit induction proof in separation logic. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 659\u2013676. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-48989-6_40"},{"key":"4_CR25","doi-asserted-by":"crossref","unstructured":"van Tonder, R., Le Goues, C.: Static automated program repair for heap properties. In: International Conference on Software Engineering (ICSE), pp. 151\u2013162 (2018)","DOI":"10.1145\/3180155.3180250"},{"key":"4_CR26","doi-asserted-by":"crossref","unstructured":"Verma, S., Roy, S.: Synergistic debug-repair of heap manipulations. In: Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC\/FSE), pp. 163\u2013173 (2017)","DOI":"10.1145\/3106237.3106263"},{"issue":"5","key":"4_CR27","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1145\/1735223.1735249","volume":"53","author":"W Weimer","year":"2010","unstructured":"Weimer, W., Forrest, S., Le Goues, C., Nguyen, T.: Automatic program repair with evolutionary computation. Commun. ACM 53(5), 109\u2013116 (2010)","journal-title":"Commun. ACM"},{"key":"4_CR28","doi-asserted-by":"crossref","unstructured":"Xin, Q., Reiss, S.P.: Identifying test-suite-overfitted patches through test case generation. In: International Symposium on Software Testing and Analysis, pp. 226\u2013236 (2017)","DOI":"10.1145\/3092703.3092718"},{"key":"4_CR29","doi-asserted-by":"crossref","unstructured":"Yang, J., Zhikhartsev, A., Liu, Y., Tan, L.: Better test cases for better automated program repair. In: Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC\/FSE), pp. 831\u2013841 (2017)","DOI":"10.1145\/3106237.3106274"},{"key":"4_CR30","unstructured":"Yu, Z., Martinez, M., Danglot, B., Durieux, T., Monperrus, M.: Test case generation for program repair: a study of feasibility and effectiveness. CoRR abs\/1703.00198 (2017)"}],"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-030-11245-5_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,1,10]],"date-time":"2019-01-10T13:46:29Z","timestamp":1547127989000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-11245-5_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030112448","9783030112455"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-11245-5_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Cascais","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 January 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 January 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/popl19.sigplan.org\/track\/VMCAI-2019","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}