基于不变式的程序修复

本文描述了一个基于程序不变式概念的正式通用自动程序修复（APR）框架。在所提出的修复框架中，动态分析缺陷程序的执行轨迹以推断规范 $\varphi_{correct}$ 和 $\varphi_{violated}$，其中 $\varphi_{correct}$ 代表运行成功所需的可能不变式集合（良好模式），而 $\varphi_{violated}$ 代表导致缺陷程序中错误的可疑不变式集合（不良模式）。然后使用严格的程序分析技术细化这些规范，这些技术也用于驱动修复过程生成可行的补丁并评估生成补丁的正确性。我们通过开发一个针对性能错误的基于不变式的修复系统，展示了在 APR 中利用不变式的有用性。初步分析表明，基于不变式的 APR 在处理性能错误方面是有效的，它能生成确保程序效率提升而不 adversely 影响其功能的补丁。