抽象解释的正确核
Correctness Kernels of Abstract Interpretations
摘要：
在基于抽象解释的静态分析中，近似是由抽象域编码的。它们为设计抽象语义函数提供了系统的指导，这些抽象语义函数近似于分析中的某些具体系统行为。为了近似给定的具体语义功能，抽象域可能包含冗余信息。本文介绍了抽象解释的正确性核的概念，一种简化抽象域的方法，即从它们中删除抽象值，以最大的方式，同时保留完全相同的近似行为的系统分析。我们表明，在抽象的模型检验正确性内核提供了一个由示例指导的抽象状态空间的简化范例，这意味着这种简化保留了示例的虚假性（即，抽象路径）。特别是，我们展示了如何正确的内核可以集成与著名的CEGAR（反例引导的抽象细化）方法。
英文摘要：
In abstract interpretation-based static analysis, approximation is encoded by abstract domains. They provide systematic guidelines for designing abstract semantic functions that approximate some concrete system behaviors under analysis. It may happen that an abstract domain contains redundant information for the specific purpose of approximating a given concrete semantic function. This paper introduces the notion of correctness kernel of abstract interpretations, a methodology for simplifying abstract domains, i.e. removing abstract values from them, in a maximal way while retaining exactly the same approximate behavior of the system under analysis. We show that in abstract model checking correctness kernels provide a simplification paradigm of the abstract state space that is guided by examples, meaning that this simplification preserves spuriousness of examples (i.e., abstract paths). In particular, we show how correctness kernels can be integrated with the well-known CEGAR (CounterExample-Guided Abstraction Refinement) methodology.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
