Our Research Program
A detailed write-up of our research on program repair appears at https://abhikrc.com/projects/Repair/index.html.
Goals
At the program level, we seek to establish automated program repair as a core scientific discipline, where the patches generated by automated program repair are trustworthy. This requires us not only to combat over-fitting in automated repair, but also to provide more scientific foundations of the repair process. This is achieved by designing repair as guided by analysis summaries, failed verification proofs and systematic test generation.
Another outcome of our research program is a family of future automated program repair tools, which can produce repairs accompanied by evidence of correctness, thereby providing ultimate correctness assurance about the patches.
Finally, the foundations/tools will support applications of program repair, including: (a) managing Application Programming Interfaces of libraries (e.g., Blue-Pencil5), (b) patches of major open-source projects (e.g., Linux), (c) repair for intelligent tutoring.
Main Deliverable: RAVE
Our research program will lead to an extensible integrated environment for continuous software development with the aid of machine-assisted program Repair, Analysis & Verification Engine, which we call RAVE. Apart from manually provided tests, RAVE will rely on a suite of static analysers, verifiers and test generators. Our vision is continuous program repair via analysis/verification/test-generation.
Work Packages
- WP1 Program Analysis
- WP2 Proof-Based Repair
- WP3 Gradual Correctness
- WP4 Environment & Deployment
Work Package 1: Program Analysis
In automated program repair, a search for a bugfix is guided by a mechanism to distinguish between "correct" and "buggy" behaviors of a program, in an attempt to eliminate the latter. In our approach, the role of such methodology will be played by a family of static program analyses, which will form the bedrock of our APR framework. Unlike testing-based approaches, static analyses infer properties of programs without executing them, thus, accounting for all possible run-time executions, and therefore, side-stepping the over-fitting issue altogether.
In this work package, we will focus on novel practical and theoretical aspects of designing, enhancing, and engineering static program analyses, as they are employed by automated program repair.
Work Package 2: Proof-based Repair
The last decade has seen a surge of large software systems that have been fully verified for a range of domain-specific (i.e., deep) functional correctness properties, using foundational or light-weight deductive verification tools. Those systems include compilers, file systems, operating systems, and even distributed applications. Due to the recent advances in proof automation those verification efforts frequently require only a modest amount of input from the user, necessary to boot-strap the verification of the properties of interest, with the rest of reasoning performed with the help of domain-specific solvers. What is even more remarkable, having a fully verified codebase with ascribed specifications, it is possible to extend it with new functionality by automatically generating programs, along with the machine-checkable proofs of their correctness, using the techniques for deductive (proof-driven) program synthesis.
In this work package we are going to harness the recent advances in deductive program verification and synthesis for building novel program repair approaches, targeting non-trivial deficiencies in software that fall beyond the scope of what can be discovered and validated by fully-automated static analysis tools.
Work Package 3: Gradual Correctness
Current state-of-the-art in program repair guides the repair process by a (manually provided) test-suite. Since the test-suite does not capture all behaviors the repairs generated may be over-fitting. Thus, it is useful to guide the repair process through more "formal" program artifacts such as analysis summaries and failed proofs as we saw in WP1 and WP2. In WP3, we will study the possibility of using automatically generated tests via a systematic test generation method to guide repair. The advantage of using tests is that for the produced repairs, these additional generated tests can be given as evidence of correctness of the repair to the developers, with a goal of engendering their trust in the patches.
Work Package 4: Environment & Deployment
In this work package we will study the applications of the automated program repair techniques developed in WP1-3, specifically into integrated program construction and protection environments. The key challenge here is to integrate it into development workflows in such a way that the generated repairs are trustworthy, and are useful for creating a sustainable and maintainable code-base over the long term.
Thus our goal is: Create trust -> Provide convenience -> Facilitate applications.
