Automated Repair of Heap-Manipulating Programs using Deductive Synthesis
We propose a novel method to automatically repairing buggy heap-manipulating programs using constraint solving and deductive synthesis. Given an input program C and its formal specification in the form of a Hoare triple: {P} C {Q}, we use a separation-logic-based verifier to verify if program C is correct w.r.t. its specifications. If program C is found buggy, we then repair it in the following steps. First, we rely on the verification results to collect a list of suspicious statements of the buggy program. For each suspicious statement, we temporarily replace it with a template patch representing the desired statements. The template patch is also formally specified using a pair of unknown pre- and postcondition. Next, we use the verifier to analyze the temporarily patched program to collect constraints related to the pre- and postcondition of the template patch. Then, these constraints are solved by our constraint solving technique to discover the suitable specifications of the template patch. Subsequently, these specifications can be used to synthesize program statements of the template patch, consequently creating a candidate program. Finally, if the candidate program is validated, it is returned as the repaired program. We demonstrate the effectiveness of our approach by evaluating our implementation and a state-of-the-art approach on a benchmark of 231 buggy programs. The experiment results show that our tool successfully repairs 223 buggy programs and considerably outperforms the compared tool.
Mon 18 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
18:30 - 19:15 | |||
18:30 15mTalk | Approximate Bit Dependency Analysis to Identify Program Synthesis Problems as Infeasible VMCAI Marius Kamp Friedrich-Alexander University Erlangen-Nürnberg, Michael Philippsen Friedrich-Alexander University Erlangen-Nürnberg (FAU) Media Attached | ||
18:45 15mTalk | Automated Repair of Heap-Manipulating Programs using Deductive Synthesis VMCAI Thanh-Toan Nguyen National University of Singapore, Quang-Trung Ta National University of Singapore, Ilya Sergey Yale-NUS College and National University of Singapore, Wei-Ngan Chin National University of Singapore Media Attached | ||
19:00 15mTalk | GPURepair: Automated Repair of GPU Kernels VMCAI Media Attached |