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.

翻译：本文提出了一种基于程序不变量概念的通用自动化程序修复（APR）形式化框架。在所述修复框架中，通过动态分析缺陷程序的执行轨迹，推断出规格说明 $\varphi_{correct}$ 和 $\varphi_{violated}$，其中 $\varphi_{correct}$ 表示成功运行所需的一组可能不变量（良好模式），$\varphi_{violated}$ 表示导致缺陷程序中出现错误的一组可疑不变量（不良模式）。随后，利用严格的程序分析技术对这些规格说明进行精化，同时这些技术也被用于驱动修复过程，以生成可行的补丁并评估所生成补丁的正确性。我们通过开发一个针对性能缺陷的基于不变量的修复系统，展示了在APR中利用不变量的实用性。初步分析表明，基于不变量的APR在处理性能缺陷时具有有效性，能够生成确保程序效率提升而不对其功能产生负面影响的补丁。