×

Automated program repair using formal verification techniques. (English) Zbl 07724872

Raskin, Jean-François (ed.) et al., Principles of systems design. Essays dedicated to Thomas A. Henzinger on the occasion of his 60th birthday. Cham: Springer. Lect. Notes Comput. Sci. 13660, 511-534 (2022).
Summary: We focus on two different approaches to automatic program repair, based on formal verification methods. Both repair techniques consider infinite-state C-like programs, and consist of a generate-validate loop, in which potentially repaired programs are repeatedly generated and verified. Both approaches are incremental – partial information gathered in previous verification attempts is used in the next steps. However, the settings of both approaches, including their techniques for finding repairs, are quite distinct. The first approach uses syntactic mutations to repair sequential programs with respect to assertions in the code. It is based on a reduction to the problem of finding unsatisfiable sets of constraints, which is addressed using an interplay between SAT and SMT solvers. A novel notion of must-fault-localization enables efficient pruning of the search space, without losing any potential repair. The second approach uses an Assume-Guarantee (AG) style reasoning in order to verify large programs, composed of two concurrent components. The AG reasoning is based on automata-learning techniques. When verification fails, the procedure repeatedly repairs one of the components, until a correct repair is found. Several different repair methods are considered, trading off precision and convergence to a correct repair.
For the entire collection see [Zbl 1516.68022].

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)

Software:

z3; Qlose; Codeflaws; Angelix; CBMC
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] https://github.com/hadarlh/AGR
[2] Albarghouthi, A., Dillig, I., Gurfinkel, A.: Maximal specification synthesis. In: POPL 51(1), 789-801(2016) · Zbl 1347.68067
[3] Alpern, B., Wegman, M.N., Zadeck, F.K.: Detecting equality of variables in programs. In: POPL (1988)
[4] Angluin, D., Learning regular sets from queries and counterexamples, Inf. Comput., 75, 2, 87-106 (1987)
[5] Assiri, FY; Bieman, JM; Arai, K.; Kapoor, S.; Bhatia, R., MUT-APR: mutation-based automated program repair research tool, Advances in Information and Communication Networks, 256-270 (2019), Cham: Springer, Cham
[6] 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-25 (2017)
[7] Bloem, R.; Drechsler, R.; Fey, G.; Finder, A.; Hofferek, G.; Könighofer, R.; Raik, J.; Repinski, U.; Sülflow, A.; Biere, A.; Nahir, A.; Vos, T., FoREnSiC- an automatic debugging environment for C programs, Hardware and Software: Verification and Testing, 260-265 (2013), Heidelberg: Springer, Heidelberg
[8] Chaki, S.; Strichman, O.; Grumberg, O.; Huth, M., Optimized L*-based assume-guarantee reasoning, Tools and Algorithms for the Construction and Analysis of Systems, 276-291 (2007), Heidelberg: Springer, Heidelberg · Zbl 1147.68568
[9] Chen, Y-F; Clarke, EM; Farzan, A.; Tsai, M-H; Tsay, Y-K; Wang, B-Y; Touili, T.; Cook, B.; Jackson, P., Automated assume-guarantee reasoning through implicit learning, Computer Aided Verification, 511-526 (2010), Heidelberg: Springer, Heidelberg
[10] Chen, Y-F; Farzan, A.; Clarke, EM; Tsay, Y-K; Wang, B-Y; Kowalewski, S.; Philippou, A., Learning minimal separating DFA’s for compositional verification, Tools and Algorithms for the Construction and Analysis of Systems, 31-45 (2009), Heidelberg: Springer, Heidelberg · Zbl 1234.68166
[11] Clarke, E.; Kroening, D.; Lerda, F.; Jensen, K.; Podelski, A., A tool for checking ANSI-C programs, Tools and Algorithms for the Construction and Analysis of Systems, 168-176 (2004), Heidelberg: Springer, Heidelberg · Zbl 1126.68470
[12] 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-371 IEEE (2003)
[13] Cobleigh, JM; Giannakopoulou, D.; Păsăreanu, CS; Garavel, H.; Hatcliff, J., Learning assumptions for compositional verification, Tools and Algorithms for the Construction and Analysis of Systems, 331-346 (2003), Heidelberg: Springer, Heidelberg
[14] D’Antoni, L.; Samanta, R.; Singh, R.; Chaudhuri, S.; Farzan, A., Qlose: program repair with quantitative objectives, Computer Aided Verification, 383-401 (2016), Cham: Springer, Cham
[15] de Moura, L.; Bjørner, N.; Ramakrishnan, CR; Rehof, J., Z3: an efficient SMT solver, Tools and Algorithms for the Construction and Analysis of Systems, 337-340 (2008), Heidelberg: Springer, Heidelberg
[16] 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-74. IEEE (2010)
[17] Dillig, I.; Dillig, T.; Sharygina, N.; Veith, H., Explain: a tool for performing abductive inference, Computer Aided Verification, 684-689 (2013), Heidelberg: Springer, Heidelberg
[18] Do, H.; Elbaum, S.; Rothermel, G., Supporting controlled experimentation with testing techniques: an infrastructure and its potential impact, Empir. Softw. Eng., 10, 4, 405-435 (2005)
[19] Elkader, KA; Grumberg, O.; Păsăreanu, CS; Shoham, S.; Bjørner, N.; de Boer, F., Automated circular assume-guarantee reasoning, FM 2015: Formal Methods, 23-39 (2015), Cham: Springer, Cham · Zbl 1427.68194
[20] Abd Elkader, K.; Grumberg, O.; Păsăreanu, CS; Shoham, S.; Chaudhuri, S.; Farzan, A., Automated circular assume-guarantee reasoning with N-way decomposition and alphabet refinement, Computer Aided Verification, 329-351 (2016), Cham: Springer, Cham · Zbl 1411.68056
[21] Frenkel, H.: Automata over infinite data domains: learnability and applications in program verification and repair, Ph. D thesis (2021)
[22] Frenkel, H.; Grumberg, O.; Păsăreanu, C.; Sheinvald, S., Assume, guarantee or repair, Tools and Algorithms for the Construction and Analysis of Systems, 211-227 (2020), Cham: Springer, Cham · Zbl 1507.68186
[23] Gheorghiu, M.; Giannakopoulou, D.; Păsăreanu, CS; Grumberg, O.; Huth, M., Refining interface alphabets for compositional verification, Tools and Algorithms for the Construction and Analysis of Systems, 292-307 (2007), Heidelberg: Springer, Heidelberg · Zbl 1186.68290
[24] Giannakopoulou, D., Păsăreanu, C.S., Barringer, H.: Assumption Generation for Software Component Verification. In: IEEE Computer Society. ASE (2002)
[25] Giannakopoulou, D.; Păsăreanu, CS; Barringer, H., Component verification with automatically generated assumptions, Autom. Softw. Eng., 12, 3, 297-320 (2005)
[26] Gupta, A.; McMillan, KL; Fu, Z., Automated assumption generation for compositional verification, Formal Methods Syst. Des., 32, 3, 285-301 (2008)
[27] Jobstmann, B.; Griesmayer, A.; Bloem, R.; Etessami, K.; Rajamani, SK, Program repair as a game, Computer Aided Verification, 226-238 (2005), Heidelberg: Springer, Heidelberg · Zbl 1081.68572
[28] Kneuss, E.; Koukoutos, M.; Kuncak, V.; Kroening, D.; Păsăreanu, CS, Deductive program repair, Computer Aided Verification, 217-233 (2015), Cham: Springer, Cham
[29] Könighofer, R., Bloem, R.: Automated error localization and correction for imperative programs. In: Formal Methods in Computer-Aided Design (FMCAD), pp. 91-100. IEEE (2011)
[30] Könighofer, R.; Bloem, R.; Biere, A.; Nahir, A.; Vos, T., Repair with on-the-fly program analysis, Hardware and Software: Verification and Testing, 56-71 (2013), Heidelberg: Springer, Heidelberg
[31] Le Goues, C.; Nguyen, T.; Forrest, S.; Weimer, W., GenProg: a generic method for automatic software repair, Softw. Eng. IEEE Trans., 38, 1, 54-72 (2012)
[32] Li, B.; Dillig, I.; Dillig, T.; McMillan, K.; Sagiv, M.; Piterman, N.; Smolka, SA, Synthesis of circular compositional program proofs via abduction, Tools and Algorithms for the Construction and Analysis of Systems, 370-384 (2013), Heidelberg: Springer, Heidelberg
[33] Lin, S-W; Hsiung, P-A; Jones, C.; Pihlajasaari, P.; Sun, J., Compositional synthesis of concurrent systems through causal model checking and learning, FM 2014: Formal Methods, 416-431 (2014), Cham: Springer, Cham
[34] 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-113 (2019)
[35] Magee, J., Kramer, J.: Concurrency - State Models and Java Programs. Wiley (1999) · Zbl 0924.68026
[36] McMillan, KL; Pierre, L.; Kropf, T., Circular compositional reasoning about liveness, Correct Hardware Design and Verification Methods, 342-346 (1999), Heidelberg: Springer, Heidelberg
[37] Mechtaev, S., Nguyen, M.-D., Noller, Y., Grunske, L., Roychoudhury, A.: Semantic program repair using a reference implementation. In: ICSE, pp. 129-139 (2018)
[38] Mechtaev, S., Yi, J., Roychoudhury, A.: Angelix: scalable multiline program patch synthesis via symbolic analysis. In: ICSE, ICSE (2016)
[39] Misra, J.; Chandy, KM, Proofs of networks of processes, IEEE Trans. Software Eng., 7, 4, 417-426 (1981) · Zbl 0468.68030
[40] Namjoshi, KS; Trefler, RJ; Emerson, EA; Sistla, AP, On the completeness of compositional reasoning, Computer Aided Verification, 139-153 (2000), Heidelberg: Springer, Heidelberg
[41] 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-781. IEEE Press (2013)
[42] Nguyen, TV; Weimer, W.; Kapur, D.; Forrest, S.; Legay, A.; Margaria, T., Connecting Program Synthesis and Reachability: Automatic Program Repair Using Test-Input Generation, Tools and Algorithms for the Construction and Analysis of Systems, 301-318 (2017), Heidelberg: Springer, Heidelberg · Zbl 1452.68052
[43] Nguyen, T-T; Ta, Q-T; Chin, W-N; Enea, C.; Piskac, R., Automatic program repair using formal verification and expression templates, Verification, Model Checking, and Abstract Interpretation, 70-91 (2019), Cham: Springer, Cham · Zbl 1522.68159
[44] Păsăreanu, 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-205 (2008). doi:10.1007/s10703-008-0049-6 · Zbl 1147.68053
[45] Peirce, C., Hartshorne, C.: Collected papers of charles sanders peirce. Belknap Press (1932)
[46] Pnueli, A.: In transition from global to modular temporal reasoning about programs. In: Logics and Models of Concurrent Systems, NATO ASI Series (1985) · Zbl 0578.68014
[47] 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-6. IEEE (2012)
[48] Rothenberg, B.-C.: Formal automated program repair, Ph. D. thesis (2020)
[49] Rothenberg, B-C; Grumberg, O.; Fitzgerald, J.; Heitmeyer, C.; Gnesi, S.; Philippou, A., Sound and complete mutation-based program repair, FM 2016: Formal Methods, 593-611 (2016), Cham: Springer, Cham · Zbl 1427.68052
[50] Rothenberg, B-C; Grumberg, O.; Lahiri, SK; Wang, C., Must fault localization for program repair, Computer Aided Verification, 658-680 (2020), Cham: Springer, Cham · Zbl 1478.68058
[51] Singh, R.; Giannakopoulou, D.; Păsăreanu, C.; Touili, T.; Cook, B.; Jackson, P., Learning component interfaces with may and must abstractions, Computer Aided Verification, 527-542 (2010), Heidelberg: Springer, Heidelberg
[52] 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-182 (2017)
[53] von Essen, C.; Jobstmann, B., Program repair without regret, Formal Methods Syst. Des., 47, 1, 26-50 (2015)
[54] Weispfenning, V.; Müller, GH; Richter, MM, Quantifier elimination and decision procedures for valued fields, Models and Sets, 419-472 (1984), Heidelberg: Springer, Heidelberg
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.