一句话：提出基于改进图数据结构与算法的 Zones 和 Octagons 抽象域快速实现，显著提升静态分析性能与验证效果。
Zones 与 Octagons 是静态程序分析中常用的抽象域，用于自动发现程序变量之间的简单数值关系。二者数学基础清晰，但具体实现面临诸多算法挑战。本文重新研究这两个抽象域及其实现和使用，针对表示差分约束的图，采用改进的数据结构与算法，构建共享基础设施上的快速实现。作者在标准基准上比较同类精度的替代方法，测量速度与精度，并在软件验证场景中考察精度提升对验证结果的影响。实验表明，新实现显著推进了 Zones 和 Octagons 的当前技术水平。
Zones and Octagons are popular abstract domains for static program analysis. They enable the automated discovery of simple numerical relations that hold between pairs of program variables. Both domains are well understood mathematically but the detailed implementation of static analyses based on these domains poses many interesting algorithmic challenges. In this article, we study the two abstract domains, their implementation and use. Utilizing improved data structures and algorithms for the manipulation of graphs that represent difference-bound constraints, we present fast implementations of both abstract domains, built around a common infrastructure. We compare the performance of these implementations against alternative approaches offering the same precision. We quantify the differences in performance by measuring their speed and precision on standard benchmarks. We also assess, in the context of software verification, the extent to which the improved precision translates to better verification outcomes. Experiments demonstrate that our new implementations improve the state of the art for both Zones and Octagons significantly.
@article{paperbot1214,
title = {A Fresh Look at Zones and Octagons},
author = {Graeme Gange and Zequn Ma and Jorge A. Navas and Peter Schachte and Harald Søndergaard and Peter J. Stuckey},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {43},
number = {3},
year = {2021},
doi = {10.1145/3457885}
}