Richard M. Karp Distinguished Lecture — Automated Formal Program Repair

In the process of software development and maintenance, much effort is invested in order to ensure that the product is as bug free as possible. Automating the repair process is highly desired. In this talk we present two approaches to automated program repair, based on formal methods. Given a buggy program, the first approach focuses on the notion of fault localization, whose goal is to point to locations in the program that might be responsible for a bug. We define the notion of must fault localization, explain its power and show how it can significantly improve the performance of the repair tool AllRepair. The approach guarantees soundness and completeness with respect to a bounded notion of correctness. The second approach intertwines compositional Assume-Guarantee verification with repair. Automata learning is used in the compositional verification. If an erroneous behavior is found, abduction assists in repairing the system by inferring new constraints that eliminate erroneous runs. Then the verification proceeds for the repaired system.

This is a joint work with Hadar Frenkel, Corina Pasareanu, Bat-chen Rothenberg, and Sarai Sheinvald.

If you require accommodation for communication, please contact our Access Coordinator at simonsevents [at] berkeley.edutarget="_blank" with as much advance notice as possible.