一句话：提出并形式化离线与在线元抽象解释，用抽象解释分析程序分析器，并据此设计更高效精确的静态分析算法。
论文提出 A²I（抽象解释的抽象解释，亦称元抽象解释），核心思想是将抽象解释应用于基于抽象解释的静态程序分析，从而分析程序分析器自身的性质。文章区分离线 A²I 与在线 A²I：前者在分析前后进行，如 Astrée 的变量打包与告警诊断；后者在分析过程中进行，如 Venet 的余纤维域以及 Halbwachs 等和 Singh 等的变量划分技术。作者对二者给出形式化，并通过 widening 的设计和关系抽象域的分解来说明该概念，展示如何把新的静态分析提取为元抽象解释，以设计高效且精确的程序分析算法。
The fundamental idea of Abstract 2 Interpretation (A 2 I), also called meta-abstract interpretation, is to apply abstract interpretation to abstract interpretation-based static program analyses. A 2 I is generally meant to use abstract interpretation to analyse properties of program analysers. A 2 I can be either offline or online. Offline A 2 I is performed either before the program analysis, such as variable packing used by the Astrée program analyser, or after the program analysis, such as in alarm diagnosis. Online A 2 I is performed during the program analysis, such as Venet’s cofibred domains or Halbwachs et al.’s and Singh et al.’s variable partitioning techniques for fast polyhedra/numerical abstract domains. We formalize offline and online meta-abstract interpretation and illustrate this notion with the design of widenings and the decomposition of relational abstract domains to speed-up program analyses. This shows how novel static analyses can be extracted as meta-abstract interpretations to design efficient and precise program analysis algorithms.
@article{paperbot636,
title = {A²I: abstract² interpretation},
author = {Patrick Cousot and Roberto Giacobazzi and Francesco Ranzato},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {POPL},
year = {2019},
doi = {10.1145/3290355}
}