一句话：提出相关性抽象域，自动推断程序输入输出间的相等关系，并用于生成 frame conditions、简化微内核不变式证明。
论文针对程序验证中 frame conditions 难以自动推断的问题，提出表示程序输入与输出部分之间相等关系的“相关性”抽象域。作者形式化相关性理论并在证明助手中机器验证其语义性质，随后为带代数数据类型和数组的一阶语言设计跨过程静态数据流分析，自动推断相关性。该分析在工业规模微内核的代码与函数规约上评估了精度和执行开销；利用推断出的相关性，能够自动消解与该微内核不变式保持相关的三分之二证明义务。
We introduce the abstract domain of correlations to denote equality relations between parts of inputs and outputs of programs. We formalise the theory of correlations, and mechanically verify their semantic properties. We design a static inter-procedural dataflow analysis for automatically inferring correlations for programs written in a first-order language equipped with algebraic data-types and arrays. The analysis, its precision and execution cost, have been evaluated on the code and functional specification of an industrial-size micro-kernel. We exploit the inferred correlations to automatically discharge two thirds of the proof obligations related to the preservation of invariants for this micro-kernel.
@article{paperbot617,
title = {Inferring frame conditions with static correlation analysis},
author = {Oana F. Andreescu and Thomas Jensen and Stéphane Lescuyer and Benoît Montagu},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {POPL},
year = {2019},
doi = {10.1145/3290360}
}