Value-based static analysis techniques express computed program invariants as logical formula over program variables. Researchers and practitioners use these invariants to aid in software engineering and verification tasks. When selecting abstract domains, practitioners weigh the cost of a domain against its expressiveness. However, an abstract domain's expressiveness tends to be stated in absolute terms; either mathematically via the sub-polyhedra the domain is capable of describing, empirically using a set of known properties to verify, or empirically via logical entailment using the entire invariant of the domain at each program point. Due to carry-over effects, however, the last technique can be problematic because it tends to provide a simplistic and imprecise comparisons. We address limitations of comparing, in general, abstract domains via logical entailment in this work. We provide a fixed-point algorithm for including the minimally necessary variables from each domain into the compared formula. Furthermore, we empirically evaluate our algorithm, comparing different techniques of widening over the Zones domain and comparing Zones to an incomparable Relational Predicates domain. Our empirical evaluation of our technique shows an improved granularity of comparison. It lowered the number of more precise invariants when comparing analysis techniques, thus, limiting the prevalent carry-over effects. Moreover, it removed undecidable invariants and lowered the number of incomparable invariants when comparing two incomparable relational abstract domains.

翻译：基于值的静态分析技术将计算得到的程序不变量表示为关于程序变量的逻辑公式。研究人员和从业者利用这些不变量辅助软件工程与验证任务。在选择抽象域时，从业者会权衡该域的成本与表达能力。然而，抽象域的表达能力往往以绝对方式陈述：要么通过该域能够描述的子多面体在数学上定义，要么通过一组已知属性进行经验验证，要么通过在每个程序点上使用该域的整个不变量进行逻辑蕴含经验验证。但由于遗留效应，后一种方法可能存在局限，因为它倾向于提供简单且不精确的比较。本文旨在解决通过逻辑蕴含比较抽象域（一般意义上的）的局限性。我们提出了一种不动点算法，用于将每个域中最少必要的变量纳入被比较的公式中。此外，我们通过实验评估了该算法，比较了Zones域上不同的扩宽技术，并将Zones域与不可比较的关系型谓词域进行了对比。实证评估表明，我们的技术提升了比较的粒度：它降低了分析技术比较中更精确不变量的数量，从而限制了普遍存在的遗留效应；同时，在比较两个不可比较的关系型抽象域时，它消除了不可判定的不变量，并降低了不可比较不变量的数量。