Christian von Essen, Barbara Jobstmann
Program Repair Revisited (2012)
Program Repair Revisited (2012)
TR-2012-4.pdf
Keywords: Synthesis, Program Repair, Sketching
Abstract: We present a new and flexible approach to repair reactive programs with respect to a specification. The specification is given in linear-temporal logic. Like in previous approaches, we require that a repaired program satisfies the specification and is syntactically close to the faulty program. In addition our approach also allows the user to ask for a program that is semantically close by enforcing that a specific subset of the correct traces is preserved. Our approach is based on synthesizing a program producing a set of traces that stays within a lower and an upper bound. We provide an algorithm to decide if a program is repairable with respect to our new notion and synthesize a repair if one exists. We analyze several ways to choose the set of traces to leave intact and show the boundaries they impose on repairability.
