一句话：提出用程序不变式形式化刻画循环程序中的性能缺陷，并支持补丁的形式化验证与加速评估。
本文针对循环程序中的性能缺陷提出形式化修复框架。性能缺陷指程序语义正确、却因某些输入执行低效的错误，传统基于测试的补丁验证无法形式化保证补丁质量。作者基于“存在性能缺陷的程序仍是语义正确的程序”这一观察，引入程序不变式来形式化处理性能缺陷：在原程序上增加若干非功能变量，用导出的不变式评估补丁版本相对原版本的执行效率。该框架有两大优势：一是可用程序验证器对补丁进行形式化验证；二是可量化补丁带来的效率提升。作者指出，这是此前文献中未被研究过的性能缺陷形式化处理方向。
This paper describes a formal repair framework for performance bugs in loop programs, which are programming errors that slow down program execution. The approach is developed based on the observation that a program with a performance bug is a semantically correct program, but it may perform inefficiently for some inputs. This observation permits the formal treatment of performance bugs using the idea of program invariants, where the original program is augmented with a number of non-functional variables that are used to assess the efficiency of the patched version vs. the original program using the derived invariants. The proposed approach offers two major advantages compared to the conventional test-based patch validation approach. First, it enables the formal validation of patches using program verifiers. Second, it helps to assess the efficiency boost provided by the generated patches. To the best of our knowledge, the formal treatment of performance bugs has not been studied in the prior literature.