אירועים והרצאות בפקולטה למדעי המחשב ע"ש הנרי ומרילין טאוב

The manual detection, examination and repair of computer bugs are all notoriously difficult tasks that programmers face daily. Automated program repair receives a program with a bug, and outputs a set of changes to the program that would make it bug-free. We focus on formal program repair, which means that programs are repaired with respect to a formal specification. Formal program repair, in contrast to test-based repair, guarantees that programs meet the specification for all inputs, and not just a selected set. In this talk, we portray the challenges posed by the formal repair problem, and discuss our approach for overcoming them. We present several algorithms developed as part of this research, which make use of mathematical and logical tools from the world of program verification, such as constraint solvers and software model checkers. We have implemented these algorithms and have tested them for the repair of buggy student submissions to programming assignments. Our results show that our algorithms are capable of producing effective repairs for these submissions, very efficiently.