Ph.D Thesis

Ph.D StudentRothenberg Bat-Chen
SubjectFormal Automated Program Repair
DepartmentDepartment of Computer Science
Supervisor PROFESSOR EMERITUS Orna Grumberg
Full Thesis textFull thesis text - English Version


Nowadays, software systems can be found not only on our laptops, but all around us: in phones, TVs, cars, airplanes and many more. Such systems are complex and hard to design, and therefore they often reach the client while still containing many hidden bugs.

When discovered by the client, these bugs damage companies’ reputation, sometimes irreversibly. Therefore, companies make tremendous efforts to detect and repair bugs, devoting a significant percentage of the development process to these tasks.

Yet even though these efforts lead to the discovery of many bugs, still, companies are forced to prioritize their repair, and many bugs remain uncorrected. This is because human resources are limited, and manual repair of bugs is a notoriously difficult task, which often requires expertise and close acquaintance with the code under inspection.

Hence, automating program repair has always been a research challenge of much interest. In recent years, however, research in this area has seen significant progress, with the development of methods that have been shown to be useful for repairing real bugs in large-scale programs.

This thesis is concerned with automated program repair from a formal point of view.

This means that programs are repaired with respect to a formal specification. Also, formal methods from the world of program verification are used for the repair process.

We mostly focus on search-based repair, where programs are iteratively sampled from within a search space and then checked to see if they meet the specification. We present three published papers, describing several algorithms. The common goal of all

 algorithms is to make search-based repair more efficient, by pruning the search space whenever possible and by making the repeated correctness checks more efficient.