Abstract
We present a formal framework for repairing infinite-state, imperative, sequential programs, with (possibly recursive) procedures and multiple assertions; the framework can generate repaired programs by modifying the original erroneous program in multiple program locations, and can ensure the readability of the repaired program using user-defined expression templates; the framework also generates a set of inductive assertions that serve as a proof of correctness of the repaired program. As a step toward integrating programmer intent and intuition in automated program repair, we present a cost-aware formulation - given a cost function associated with permissible statement modifications, the goal is to ensure that the total program modification cost does not exceed a given repair budget. As part of our predicate abstractionbased solution framework, we present a sound and complete algorithm for repair of Boolean programs. We have developed a prototype tool based on SMT solving and used it successfully to repair diverse errors in benchmark C programs.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Arcuri, A.: On the Automation of Fixing Software Bugs. In: International Conference on Software Engineering (ICSE), pp. 1003–1006. ACM (2008)
Ball, T., Bounimova, E., Kumar, R., Levin, V.: SLAM2: Static Driver Verification with under 4% False Alarms. In: Formal Methods in Computer Aided Design (FMCAD), pp. 35–42 (2010)
Ball, T., Naik, M., Rajamani, S.K.: From Symptom to Cause: Localizing Errors in Counterexample Traces. In: Principles of Programming Languages (POPL), pp. 97–105. ACM (2003)
Ball, T., Rajamani, S.K.: Boolean Programs: A Model and Process for Software Analysis. Tech. Rep. 2000-14, MSR (2000)
Ball, T., Rajamani, S.K.: Automatically Validating Temporal Safety Properties of Interfaces. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 103–122. Springer, Heidelberg (2001)
Bloem, R., Chatterjee, K., Henzinger, T.A., Jobstmann, B.: Better Quality in Synthesis through Quantitative Objectives. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 140–156. Springer, Heidelberg (2009)
Chandra, S., Torlak, E., Barman, S., Bodik, R.: Angelic Debugging. In: International Conference on Software Engineering (ICSE), pp. 121–130. ACM (2011)
Clarke, E., Kroning, D., Sharygina, N., Yorav, K.: SATABS: SAT-based Predicate Abstraction for ANSI-C. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 570–574. Springer, Heidelberg (2005)
Competition on Software Verification (SV-COMP): Loops Benchmarks (2014), http://sv-comp.sosy-lab.org/2014/benchmarks.php
Debroy, V., Wong, W.E.: Using Mutation to Automatically Suggest Fixes for Faulty Programs. In: Software Testing, Verification and Validation (ICST), pp. 65–74 (2010)
Floyd, R.W.: Assigning Meanings to Programs. In: Mathematical Aspects of Computer Science, pp. 19–32. American Mathematical Society (1967)
Goues, C.L., Dewey-Vogt, M., Forrest, S., Weimer, W.: A Systematic Study of Automated Program Repair: Fixing 55 out of 105 Bugs for $8 Each. In: International Conference on Software Engineering (ICSE), pp. 3–13. IEEE Press (2012)
Graf, S., Saïdi, H.: Construction of Abstract State Graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)
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–371. Springer, Heidelberg (2006)
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–238. Springer, Heidelberg (2005)
Jose, M., Majumdar, R.: Cause Clue Clauses: Error Localization using Maximum Satisfiability. In: Programming Language Design and Implementation (PLDI), pp. 437–446. ACM (2011)
Könighofer, R., Bloem, R.: Automated Error Localization and Correction for Imperative Programs. In: Formal Methods in Computer Aided Design (FMCAD), pp. 91–100 (2011)
Logozzo, F., Ball, T.: Modular and Verified Automatic Program Repair. In: Object Oriented Programming Systems Languages and Applications (OOPSLA), pp. 133–146. ACM (2012)
Manna, Z.: Introduction to Mathematical Theory of Computation. McGraw-Hill, Inc. (1974)
de Moura, L., Bjørner, N.S.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
NEC: NECLA Static Analysis Benchmarks, http://www.nec-labs.com/research/system/systems_SAV-website/benchmarks.php
Samanta, R., Deshmukh, J.V., Emerson, E.A.: Automatic Generation of Local Repairs for Boolean Programs. In: Formal Methods in Computer Aided Design (FMCAD), pp. 1–10 (2008)
Samanta, R., Olivo, O., Emerson, E.A.: Cost-Aware Automatic Program Repair. CoRR abs/1307.7281 (2013)
Singh, R., Gulwani, S., Solar-Lezama, A.: Automatic Feedback Generation for Introductory Programming Assignments. In: Programming Language Design and Implementation, PLDI (2013)
Singh, R., Solar-Lezma, A.: Synthesizing Data-Structure Manipulations from Storyboards. In: Foundations of Software Engineering (FSE), pp. 289–299 (2011)
Solar-Lezama, A., Rabbah, R., Bodik, R., Ebcioglu, K.: Programming by Sketching for Bit-streaming Programs. In: Programming Language Design and Implementation (PLDI), pp. 281–294. ACM (2005)
Solar-Lezama, A., Tancau, L., Bodik, R., Seshia, S., Saraswat, V.: Combinatorial Sketching for Finite Programs. In: Architectural Support for Programming Languages and Operating Systems (ASPLOS), pp. 404–415. ACM (2006)
Srivastava, S., Gulwani, S., Foster, J.S.: From Program Verification to Program Synthesis. In: Principles of Programming Languages (POPL), pp. 313–326. ACM (2010)
Wei, Y., Pei, Y., Furia, C.A., Silva, L.S., Buchholz, S., Meyer, B., Zeller, A.: Automated Fixing of Programs with Contracts. In: International Symposium on Software Testing and Analysis (ISSTA), pp. 61–72. ACM (2010)
Nokhbeh Zaeem, R., Gopinath, D., Khurshid, S., McKinley, K.S.: History-Aware Data Structure Repair using SAT. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 2–17. Springer, Heidelberg (2012)
Zeller, A., Hilebrandt, R.: Simplifying and Isolating Failure-Inducing Input. IEEE Trans. Softw. Eng. 28(2), 183–200 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Samanta, R., Olivo, O., Emerson, E.A. (2014). Cost-Aware Automatic Program Repair. In: Müller-Olm, M., Seidl, H. (eds) Static Analysis. SAS 2014. Lecture Notes in Computer Science, vol 8723. Springer, Cham. https://doi.org/10.1007/978-3-319-10936-7_17
Download citation
DOI: https://doi.org/10.1007/978-3-319-10936-7_17
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-10935-0
Online ISBN: 978-3-319-10936-7
eBook Packages: Computer ScienceComputer Science (R0)