Toward a theory of program repair. (English) Zbl 07727458

Summary: To repair a program does not mean to make it (absolutely) correct; it only means to make it more-correct than it was originally. This is not a mundane academic distinction: given that programs typically have about a dozen faults per KLOC, it is important for program repair methods and tools to be designed in such a way that they map an incorrect program into a more-correct, albeit still potentially incorrect, program. Yet in the absence of a concept of relative correctness, many program repair methods and tools resort to approximations of absolute correctness; since these methods and tools are often validated against programs with a single fault, making them absolutely correct is indistinguishable from making them more-correct; this has contributed to conceal/obscure the absence of (and the need for) relative correctness. In this paper, we propose a theory of program repair based on a concept of relative correctness. We aspire to encourage researchers in program repair to explicitly specify what concept of relative correctness their method or tool is based upon; and to validate their method or tool by proving that it does enhance relative correctness, as defined.


68Qxx Theory of computing
Full Text: DOI


[1] Abreu, R.: Gzoltar: a toolset for automatic test suite minimization and fault identification. In: International Workshop on the Future of Debugging, Lugano, Switzerland (2013)
[2] Abrial, JR, The B Book: Assigning Programs to Meanings (1996), Cambridge: Cambridge University Press, Cambridge · Zbl 0915.68015 · doi:10.1017/CBO9780511624162
[3] Anonymous: Addendum, the bane of generate-and-validate program repair, crcfix data. Technical report. https://anonymous.4open.science/r/7c54e6e6-1c2f-491c-bf5a-d7f451fb463c/ (May 2020)
[4] Anonymous: Addendum, the bane of generate-and-validate program repair, crcfix tool. Technical report. https://anonymous.4open.science/r/95d330a9-97bf-44ab-9144-f214dce174d2/ (September 2020)
[5] Avizienis, A.; Laprie, JC; Randell, B.; Landwehr, CE, Basic concepts and taxonomy of dependable and secure computing, IEEE Trans. Dependable Secure Comput., 1, 1, 11-33 (2004) · doi:10.1109/TDSC.2004.2
[6] Bergstra, JA, Instruction sequence faults with formal change justification, Sci. Ann. Comput. Sci., 30, 2, 105-166 (2020) · Zbl 1513.68008
[7] Boudriga, N.; Elloumi, F.; Mili, A., The lattice of specifications: applications to a specification methodology, Formal Aspects Comput., 4, 6, 544-571 (1992) · Zbl 0782.68077 · doi:10.1007/BF01211474
[8] Brink, C.; Kahl, W.; Schmidt, G., Relational Methods in Computer Science. Advances in Computer Science (1997), Berlin: Springer, Berlin · Zbl 0871.00027
[9] Christakis, M., Heizmann, M., Mansur, M.N., Schilling, C., Wuestholz, V.: Semantic fault localization and suspiciousness ranking. In: Vojnar, T., Zhang, L. (eds.) Proceedings, TACAS 2019, Number 11427 in LNCS, pp. 226-243 (2019)
[10] Debroy, V.; Eric Wong, W., Combining mutation and fault localization for automated program debugging, J. Syst. Softw., 90, 45-60 (2013) · doi:10.1016/j.jss.2013.10.042
[11] DeMarco, F., Xuan, J., Berra, D.L., Monperrus, M.: Automatic repair of buggy if conditions and missing preconditions with SMT. In: Proceedings, CSTVA, pp. 30-39 (2014)
[12] Demarco, F., Xuan, J., Berre, D.L., Monperrus, M.: Automatic repair of buggy if conditions and missing preconditions with SMT. In Proceedings, CSTVA, pp. 30-39 (2014)
[13] Desharnais, J., Diallo, N., Ghardallou, W., Frias, M.F., Jaoua, A., Mili, A.: Relational mathematics for relative correctness. In: RAMICS, 2015, volume 9348 of LNCS, Braga, Portugal. Springer, pp 191-208, September (2015) · Zbl 1471.68057
[14] Desharnais, J., Diallo, N., Ghardallou, W., Ali, M.: Definitions and implications. In: Science of Computer Programming, Projecting programs on specifications (2017) · Zbl 1395.68091
[15] Diallo, N.; Ghardallou, W.; Desharnais, J.; Frias, M.; Jaoua, A.; Mili, A., What is a fault? and why does it matter?, ISSE, 19, 219-239 (2017)
[16] Dijkstra, EW, A Discipline of Programming (1976), Englewood Cliffs: Prentice Hall, Englewood Cliffs · Zbl 0368.68005
[17] Ermis, E., Schaef, M., Wies, T.: Error invariants. In: Giannakopoulou, D., Mery, D. (eds.) Proceedings, FM 2012, Number 7436 in LNCS, pp. 187-201 (2012) · Zbl 1372.68061
[18] Frenkel, H., Grumberg, O., Pasareanu, C., Sheinvald, S.: Assume, guarantee or repair. In: Biere, A., Parker, D. (eds.) Proceedings, TACAS 2020, Number 12078 in LNCS. Springer (2020) · Zbl 1507.68186
[19] Gazzola, L.; Micucci, D.; Mariani, L., Automatic software repair: a survey, IEEE Trans. Soft. Eng., 45, 1, 34-67 (2019) · doi:10.1109/TSE.2017.2755013
[20] Ghardallou, W., Diallo, N., Mili, A., Frias, M.: Debugging without testing. In: Proceedings, International Conference on Software Testing, Chicago, IL (April 2016)
[21] Gopinath, R., Alipour, A., Ahmed, I., Jensen, C., Groce, A.: Measuring effectiveness of mutant sets. In: Proceedings, Ninth International Conference on Software Testing, Chicago, IL, April 11-15 (2016)
[22] Gries, D., The Science of Programming (1981), New York: Springer, New York · Zbl 0472.68003 · doi:10.1007/978-1-4612-5983-1
[23] Gupta, R., Pal, S., Kanade, A., Shevade, S.K.: Deepfix: Fixing common c language errors by deep learning. In: Proceedings, AAAI, pp. 1345-1351 (2017)
[24] Hehner, ECR, A Practical Theory of Programming (1992), Englewood Cliffs: Prentice Hall, Englewood Cliffs · Zbl 0793.68002
[25] Hoare, CAR, An axiomatic basis for computer programming, Commun. ACM, 12, 10, 576-583 (1969) · Zbl 0179.23105 · doi:10.1145/363235.363259
[26] Hoare, C.A.R.: Unified theories of programming. In: Mathematical Methods in Program Development. Springer (1997) · Zbl 0884.68011
[27] IEEE Std 7-4.3.2-2003. Ieee standard criteria for digital computers in safety systems of nuclear power generating stations. Technical report, The Institute of Electrical and Electronics Engineers (2003)
[28] Jiang, J.J., Xiong, Y.F., Zhang, H.Y., Gao, Q., Chen, X.C.: Shaping program repair space with existing patches and similar code. In: Proceedings, ISSTA, pp. 298-309 (2018)
[29] Jose, M., Majumdar, R.: Cause clue clauses: error localization using maximum satisfiability. In: Proceedings, PLDI, pp. 437-446 (2011)
[30] Just, R., Jalali, D., Ernst, M.D.: Defects4j: a database of existing faults to enable controlled testing studies for java programs. In: Proceedings. ISSTA 2014, pp. 437-440. CA, USA, San Jose (July 2014)
[31] Ke, Y., Stolee, K.T., Le Goues, C., Brun, Y.: Repairing programs with semantic code search. In: International Conference on Automated Software Engineering (2015)
[32] Khaireddine, B., Martinez, M., Mili, A.: Program repair at arbitrary fault depth. In: Proceedings, ICST 2019, Xi’an, China (April 2019)
[33] Khaireddine, B., Mili, A.: Quantifying faultiness: What does it mean to have \(n\) faults? In: Proceedings, FormaliSE 2021, ICSE 2021 Colocated Conference (May 2021)
[34] Khaireddine, B., Zakharchenko, A., Mili, A.: A generic algorithm for program repair. In: Proceedings, FormaliSE, Buenos Aires, Argentina (May 2017) · Zbl 07727458
[35] Kim, D., Nam, J., Song, J., Kim, S.: Automatic patch generation learned from human-written patches. In: International Conference on Software Engineering (ICSE), pp. 802-811 (2013)
[36] Kim, D., Nam, J., Song, J., Kim, S.: Automatic patch generation learned from human-written patches. In: ICSE, pp. 802-811 (2013)
[37] Koyuncu, A., Liu, K., Bissiande, T.F., Kim, D., Klein, J., Monperrus, M., LeTraon, Y.: Fixminer: Mining relevant fix patterns for automated program repairs. In: Empirical Software Engineering, pp. 1-45 (2020)
[38] Laprie, J.C.: Dependable computing: concepts, challenges, directions. In: Proceedings, COMPSAC (2004)
[39] Le, X.-B.D., Chu, D.-H., Lo, D., Goues, C.L., Visser, W.: S3: Syntax and semantic guided repair synthesis via programming examples. In Proceedings, FSE 2017, Paderborn, Germany, September 4-8 (2017)
[40] LeGoues, C.; Forrest, S.; Weimer, W., Current challenges in automatic software repair, Softw. Qual. J., 21, 3, 421-443 (2013) · doi:10.1007/s11219-013-9208-0
[41] LeGoues, C., Dewey, V.M., Forrest, S., Weimer, W.: A systematic study of automated program repair: fixing 55 out of 105 bugs for $8 each. In: Proceedings, ICSE 2012, pp. 3-13 (2012)
[42] Li, Y., Wang, S., Nguyen, T.N.: Dlfix: context-based code transformation learning for automated program repair. In: Proceedings, ICSE 2020, Seoul, South Korea (May 2020)
[43] Le Goues, C., Nguyen, T., Forrest, S., Weimer, W.: Genprog: a generic method for automated software repair. IEEE Trans. Softw. Eng. 31(1) (2012)
[44] Lin, D., Koppel, J., Chen, A., Solar-Lezma, A.: Quixbugs: a multilingual program repair benchmark set based on the quixey challenge. In: Proceedings, SPALSH (2017)
[45] Le Goues, C.; Pradel, M.; Roychoudhury, A., Automated program repair, Commun. ACM, 62, 12, 56-65 (2019) · doi:10.1145/3318162
[46] Liu, K., et al.: Lsrepair: Live search of fix ingredients for automated program repair. In: Proceedings, 25th Asia-Pacific Software Engineering Conference. IEEE (2018)
[47] Long, F., Rinard, M.: Prophet: automatic patch generation via learning from successful patches. Technical Report Technical Report MIT-CSAIL-TR-2015, MIT (2015)
[48] Long, F., Rinard, M.: Staged program repair with condition synthesis. In: Proceedings, ESEC-FSE, (2015)
[49] Long, F., Rinard, M.: Staged program repair with condition synthesis. In: ESEC-FSE, (2015)
[50] Long, F., Rinard, M.: An analysis of the search spaces for generate-and-validate patch generation systems. In: ICSE 2016 (2016)
[51] Lou, Y., Ghanbari, A., Li, X., Zhang, L., Zhang, H., Hao, D., Zhang, L.: Can automated program repair refine fault localization? A unified debugging approach. In: Proceedings, ISSTA, pp. 75-87 (2020)
[52] Manna, Z., A Mathematical Theory of Computation (1974), New York: McGraw-Hill, New York · Zbl 0353.68066
[53] Martinez M., Monperrus M.: Mining software repair models for reasoning on the search space of automated program fixing. In: Empirical Software Engineering (2013)
[54] Martinez, M., Monperrus, M.: Astor: a program repair library for java. In: Proceedings. ISSTA 2016, pp. 441-444. Saarbrucken, Germany (2016)
[55] Martinez, M., Monperrus, M.: Astor: exploring the design space of generate-and-validate program repair beyond genprog (2018)
[56] Martinez, M., Monperrus, M.: Ultra large repair search space with automatically mined templates: the cardumen mode of astor. In: Proceedings, SSBSE, pp. 65-86 (2018)
[57] Mechtaev, S., Yi, J., Roychoudhury, A.: Angelix: scalable multiline program patch synthesis via symbolic analysis. In: Proceedings, ICSE 2016, Austin, TX (May 2016)
[58] Mili, A., Frias, M., Jaoua, A.: On faults and faulty programs. In: Hoefner, P., Jipsen, P., Kahl, W., Mueller, M.E. (eds.) Proceedings, RAMICS 2014, Volume 8428 of LNCS, pp. 191-207 (2014) · Zbl 1405.68082
[59] Mills, HD; Basili, VR; Gannon, JD; Hamlet, DR, Structured Programming: A Mathematical Approach (1986), Boston: Allyn and Bacon, Boston · Zbl 0875.68207
[60] Monperrus, M.: A critical review of patch generation learned from human written patches: essay on the problem statement and evaluation of automatic software repair. In: Proceedings, ICSE 2014, Hyderabad, India (2014)
[61] Morgan, CC, Programming from Specifications, International Series in Computer Sciences (1998), London: Prentice Hall, London
[62] Musa, JD, Operational profile in software reliability engineering, IEEE Softw., 10, 2, 14-32 (1993) · doi:10.1109/52.199724
[63] Nguyen, H.D.T., Qi, D.W., Roychoudhury, A., Chandra, S.: Semfix: Program repair via semantic analysis. In: Proceedings, ICSE, pp. 772-781 (2013)
[64] Nilizadeh, A., Calvo, M., Leavens, G.T., Cok, D.R.: Generating counter examples in the form of unit tests from hoare-style verification attempts. In: Proceedings, 32nd IEEE/ACM International Conference on Formal Methods in Software Engineering, pp. 124-128. IEEE/ACM, Pittsburgh, PA (2022)
[65] Nilizadeh, A., Calvo, M., Leavens, G.T., Le, X.-B.D.: More reliable test suites for dynamic APR by using counter-examples. In: Proceedings, 32nd IEEE International Symposium on Software Reliability Engineering, pp. 208-219. IEEE (2021)
[66] Nilizadeh, A., Leavens, G.T., Le, X.-B.D., Pasareanu, C.S., Cok, D.R.: Exploring true test overfitting in dynamic automated program repair using formal methods. In: Proceedings, 14th IEEE International Conference on Software Testing, Verification and Validation, pp. 229-240. IEEE (2021)
[67] Qi, Z., Long, F., Achour, S., Rinard, M.: An analysis of patch plausibility and correctness for generate-and-validate patch generation systems. In: Proceedings, ISSTA 2015, Baltimore, MD, July (2015)
[68] Rothenberg, B.-C., Grumberg, O.: Sound and complete mutation-based program repair. In: Proceedings, FM, pp. 593-611 (2016) · Zbl 1427.68052
[69] Rothenberg, B.-C., Grumberg, O.: Must fault localization for program repair. In: Proceedings, CAV, pp. 658-680 (2020) · Zbl 1478.68058
[70] Saha, S., Saha, R., Prasad, M.: Harnessing evolution for multi-hunk program repair. In: Proceedings, ICSE (2019)
[71] Soto, M., Le Goues, C.: Using a probabilistic model to predict bug fixes. In: Proceedings, SANER, pp. 221-231 (2018)
[72] Tan, S.H., Roychoudhury, A.: Relifix: Automated repair of software regressions. In: ICSE (2015)
[73] Weimer, W., Nguyen, T., Le Goues, C., Forrest, S.: Automatically finding patches using genetic programming. In: Proceedings, International Conference on Software Engineering (ICSE), pp. 364-374 (2009)
[74] Wen, W., Chen, J.J., Wu, R., Hao, D., Cheung, S.C.: Context-aware patch generation for better automated program repair. In: Proceedings, ICSE 2018, Gothenburg, Sweden, May 27-June 3 (2018)
[75] Wong, WR; Gao, R.; Li, YH; Abreu, R.; Wotawa, F., A survey of software fault localization, IEEE Trans. Softw. Eng., 42, 707-740 (2016) · doi:10.1109/TSE.2016.2521368
[76] Xin, Q., Reiss, S.P.: Leveraging syntax-related code for automated program repair. In: Proceedings, ASE 2017, Urbana Champaign, IL, October 30-November 3 (2017)
[77] Xiong, Y.F., Wang, J., Yan, R.F., Zhang, J.C., Han, S., Huang, G., Zhang, L.: Precise condition synthesis for program repair. In Proceedings, ICSE, pp. 416-426 (2017)
[78] Xuan, J., Martinez, M., Demarco, F., Clement, M., Lamelas Marcotte, S., Durieux, T., LeBerre, D., Monperrus, M.: Nopol: Automatic repair of conditional statement bugs in java programs. In: IEEE-TSE (2016)
[79] Xuan, J., Monperrus, M.: Test case purification for improving fault localization. In: Proceedings, FSE (2014)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.