Abstract

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.

Maple

Maple is build on top of the HIP verification system and Songbird prover.

Compared Tools

• AllRepair
• Forensic
• Angelix - The experiments are done with the provided VirtualBox image.
• GenProg

The Benchmarks and Experiments.

• The test suites for the TCAS benchmark is provided by Xianglong Kong. You can download by this link. The benchmark contains 41 buggy cases. Each case has its own test suite of 40 tests.
• The details about the second benchmark is provided in Github.
• The experiments of AllRepair and Forensic are done with the same format which uses an assertion that compares the results of buggy and correct programs, e.g. assert(buggy_sum(x, y) == correct_sum(x,y)
• For GenProg and Angelix, we create test suites of 10 for each buggy program in the second experiment. We follow their tutorials in setting up this experiment.

People

• 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)