一句话：在抽象解释中提出统一描述上下文、调用点、对象等各类敏感性技术的通用抽象域构造框架。
静态分析常使用上下文敏感、调用点敏感、对象敏感等敏感性技术来提升精度，但此前缺乏能统一描述所有常见敏感性的框架，导致涉及敏感性的分析工具其可靠性证明往往依赖临时形式化，也难发现不同技术间的相似性。本文在抽象解释中提出并形式化一个敏感性描述框架：基于一种强力的抽象域构造，利用 reduced cardinal power 将基本抽象谓词与分析所敏感的性质关联，并给出将其转化为通用抽象域构造所需的主要抽象操作。该框架能更精确地描述程序状态，统一刻画静态（分析前已知）与动态（分析中推断）敏感性准则及敏感分析调优参数，并可描述先进静态分析工具中使用的敏感性技术。
Program analyses often utilize various forms of sensitivity such as context sensitivity, call-site sensitivity, and object sensitivity. These techniques all allow for more precise program analyses, that are able to compute more precise program invariants, and to verify stronger properties. Despite the fact that sensitivity techniques are now part of the standard toolkit of static analyses designers and implementers, no comprehensive frameworks allow the description of all common forms of sensitivity. As a consequence, the soundness proofs of static analysis tools involving sensitivity often rely on ad hoc formalization, which are not always carried out in an abstract interpretation framework. Moreover, this also means that opportunities to identify similarities between analysis techniques to better improve abstractions or to tune static analysis tools can easily be missed. In this article, we present and formalize a framework for the description of sensitivity in static analysis . Our framework is based on a powerful abstract domain construction, and utilizes reduced cardinal power to tie basic abstract predicates to the properties analyses are sensitive to. We formalize this abstraction, and the main abstract operations that are needed to turn it into a generic abstract domain construction. We demonstrate that our approach can allow for a more precise description of program states, and that it can also describe a large set of sensitivity techniques, both when sensitivity criteria are static (known before the analysis) or dynamic (inferred as part of the analysis), and sensitive analysis tuning parameters. Last, we show that sensitivity techniques used in state-of-the-art static analysis tools can be described in our framework.
@article{paperbot316,
title = {A Theoretical Foundation of Sensitivity in an Abstract Interpretation Framework},
author = {Se-Won Kim and Xavier Rival and Sukyoung Ryu},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {40},
number = {3},
year = {2018},
doi = {10.1145/3230624}
}