|Title:||Formal Automated Program Repair
|Abstract:||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.|
|Copyright||The above paper is copyright by the Technion, Author(s), or others. Please contact the author(s) for more information|
|Disclaimer||Recent theses may have not yet been approved by the Technion Senate, and are provided here for the purpose of fast dissemination of knowledge only. Final approval of the Technion Senate is needed for a thesis to be used for the partial fulfillment of the requirements for the degree of M.Sc. or Ph.D.|
Remark: Any link to this technical report should be to this page (http://www.cs.technion.ac.il/users/wwwb/cgi-bin/tr-info.cgi/2020/PHD/PHD-2020-10), rather than to the URL of the PDF files directly. The latter URLs may change without notice.
To the list of the PHD technical reports of 2020
To the main CS technical reports page
Computer science department, Technion