# Connecting Program Synthesis and Reachability: Automatic Program Repair using Test-Input Generation

## TL;DR

This paper establishes a formal link between program synthesis and reachability, enabling the transfer of techniques and demonstrating a novel approach to automatic program repair using reachability tools and test-input generation.

## Contribution

It proves the equivalence between synthesis and reachability problems and develops a prototype for program repair leveraging reachability and test-input generation techniques.

## Key findings

- The approach compares favorably to existing repair methods.
- The reduction enables transfer of techniques between synthesis and reachability.
- Preliminary results show effective repair of buggy programs.

## Abstract

We prove that certain formulations of program synthesis and reachability are equivalent. Specifically, our constructive proof shows the reductions between the template-based synthesis problem, which generates a program in a pre-specified form, and the reachability problem, which decides the reachability of a program location. This establishes a link between the two research fields and allows for the transfer of techniques and results between them. To demonstrate the equivalence, we develop a program repair prototype using reachability tools. We transform a buggy program and its required specification into a specific program containing a location reachable only when the original program can be repaired, and then apply an off-the-shelf test-input generation tool on the transformed program to find test values to reach the desired location. Those test values correspond to repairs for the original programm. Preliminary results suggest that our approach compares favorably to other repair methods.