Cost-Aware Automatic Program Repair

TL;DR

This paper introduces a formal, cost-aware framework for automated program repair that modifies programs within a specified budget, ensuring correctness and readability, and demonstrates its effectiveness on benchmark C programs.

Contribution

It presents a novel cost-aware repair framework integrating programmer intent, with a sound and complete algorithm for Boolean programs and a prototype tool for C programs.

Findings

Successfully repaired diverse errors in benchmark C programs

Ensured repaired programs are readable using user-defined templates

Maintained correctness through inductive assertions

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 abstraction-based 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.