Invariant-based Program Repair
Omar I. Al-Bataineh
TL;DR
The paper addresses the challenge of low-quality patches in automated program repair due to missing specifications. It proposes an invariant-based APR that automatically infers two specifications, $\varphi_{correct}$ and $\varphi_{violated}$, from passing and failing traces and refines them with program analysis tools to guide patch generation and formal verification. The approach is applied to performance bugs, using invariants to capture non-functional requirements and validate patches, aiming to improve efficiency without sacrificing functionality. A real-world Apache bug example demonstrates the method's ability to produce valid, efficiency-enhancing patches and to reduce patch overfitting through formal invariant-based validation with tools like CPAChecker and Daikon.
Abstract
This paper describes a formal general-purpose automated program repair (APR) framework based on the concept of program invariants. In the presented repair framework, the execution traces of a defected program are dynamically analyzed to infer specifications $\varphi_{correct}$ and $\varphi_{violated}$, where $\varphi_{correct}$ represents the set of likely invariants (good patterns) required for a run to be successful and $\varphi_{violated}$ represents the set of likely suspicious invariants (bad patterns) that result in the bug in the defected program. These specifications are then refined using rigorous program analysis techniques, which are also used to drive the repair process towards feasible patches and assess the correctness of generated patches.We demonstrate the usefulness of leveraging invariants in APR by developing an invariant-based repair system for performance bugs. The initial analysis shows the effectiveness of invariant-based APR in handling performance bugs by producing patches that ensure program's efficiency increase without adversely impacting its functionality.