We present an automated approach to repair programs using formal verification and expression templates. In our approach, an input program is first verified against its formal specification to discover potentially buggy statements. For each of these statements, we identify the expression that needs to be repaired and set up a template patch which is a linear expression composed of the program's variables and unknown coefficients. Then, we analyze the template-patched program against its specification to collect a set of constraints of the template patch. This constraint set will be solved by a constraint solving technique using Farkas' lemma to identify the unknown coefficients, consequently discovering the patch. We implement our approach in a tool called {\maple} and evaluate it with various buggy programs from a widely used benchmark {\TCAS} as well as a synthetic, yet challenging benchmark containing recursive programs. Our tool outperforms state-of-the-art program repair tools in returning desired patches.
In our paper's experiment section, we have 2 benchmarks, TCAS and a newly-created Recursion. The details about the second benchmark is provided in Github.
- Dr. Wei-Ngan Chin (Associate Professor - National University of Singapore)
- Dr. Quang-Trung Ta (Research Fellow - National University of Singapore)
- Thanh-Toan Nguyen (PhD Candidate - National University of Singapore)