一句话：将抽象变换器的构造视为程序合成问题，可自动生成最精确的抽象变换器，并已在 AMURTH 中实现。
该论文研究如何自动构造静态分析器中的抽象变换器，以替代易出错的人工编写。作者将这一问题建模为程序合成：用户提供操作 op 的具体语义、抽象域 A，以及用于表达抽象变换器的领域特定语言 L；方法自动合成 op 在 A 上的 L-变换器，且保证所得变换器是相对 L 最精确的，即不存在严格更精确的 L-变换器。作者实现了 AMURTH 工具，并为两个已有分析器生成替代抽象变换器。评估表明，替换后分析器性能基本一致，同时发现原有手工变换器中有四个是不可靠的（unsound），说明手工构造存在风险。
This paper addresses the problem of creating abstract transformers automatically. The method we present automates the construction of static analyzers in a fashion similar to the way yacc automates the construction of parsers. Our method treats the problem as a program-synthesis problem. The user provides specifications of (i) the concrete semantics of a given operation op , (ii) the abstract domain A to be used by the analyzer, and (iii) the semantics of a domain-specific language L in which the abstract transformer is to be expressed. As output, our method creates an abstract transformer for op in abstract domain A , expressed in L (an “ L -transformer for op over A ”). Moreover, the abstract transformer obtained is a most-precise L -transformer for op over A ; that is, there is no other L -transformer for op over A that is strictly more precise. We implemented our method in a tool called AMURTH. We used AMURTH to create sets of replacement abstract transformers for those used in two existing analyzers, and obtained essentially identical performance. However, when we compared the existing transformers with the transformers obtained using AMURTH, we discovered that four of the existing transformers were unsound, which demonstrates the risk of using manually created transformers.
@article{paperbot1465,
title = {Synthesizing abstract transformers},
author = {Pankaj Kumar Kalita and Sujit Kumar Muduli and Loris D’Antoni and Thomas Reps and Subhajit Roy},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {OOPSLA2},
year = {2022},
doi = {10.1145/3563334}
}