Formal Verification-based Program Repair

Abstract.

Automated program repair has been an active research field in software engineering in the last decade. It aims to help developers automatically localize and fix program bugs, consequently reducing debugging efforts. Automated repair tools have been incorporated into continuous integration and code review processes to ease the debugging tasks of programmers. This dissertation proposes approaches that aim to extend the capabilities of automated program repair in various domains.

This dissertation aims to increase the effectiveness of repair approaches that use formal verification to check the correctness of a program. In this research direction, the correctness of a program is described by formal specifications, such as loop invariants, preconditions, postconditions, and assertions. Then, the correctness of a program w.r.t. its specifications is checked using formal verification. In this setup, a program is said to be buggy when it fails to meet its provided specifications. A program repair method fixes the buggy program by generating a patched program satisfying the specifications. This dissertation introduces novel approaches to formal verification-based program repair in three domains.

In the first domain, a buggy numeric program is repaired by replacing a buggy expression with a template patch, expressing the desired expression. Then, formal verification is used to collect constraints related to the template patch. Finally, the correct expression of the template patch is generated using Farkas' lemma [CSS03]. An implemented prototype of the approach outperforms state-of-the-art program repair tools in fixing buggy numeric programs in two benchmarks.

In the second domain, a buggy heap-manipulating program is fixed by substituting a buggy statement with a template patch with corresponding unknown precondition and postcondition. Then, a list of constraints related to the unknown precondition and postcondition is gathered and solved to generate the definition of the precondition and postcondition of the template patch. In the last phase, program statements of the patch are synthesized using the inferred precondition and postcondition in the previous step. In evaluation, the implementation of the proposed approach surpasses a state-of-the-art approach by a wide margin in the experiments.

In the third domain, a novel approach to fixing memory leaks is introduced. The new approach considers a limitation of current repair approaches to fixing memory leaks in that they do not consider the relation between allocated pointers. Therefore, a patch to fix a memory can lead to a new error, such as a use-after-free. The proposed approach uses separation logic to precisely capture the program state at a memory leak location to address the limitation. As a result, the approach can identify all leaked pointers at the leak location. Next, the approach uses deductive synthesis to deallocate all leaked pointers according to their shapes and in the correct sequence. A prototype is implemented and evaluated in two benchmarks. The experiment results demonstrate the effectiveness of the proposed approach in fixing complicated memory leaks involving multiple allocated pointers. Moreover, the evaluation also shows that the proposed approach can fix memory leaks in large open-source projects.