最小化比较关系抽象域
摘要：通过逻辑蕴含比较抽象域的局限性工作中，我们提供了一种固定点算法，用于将每个域中的最小必要变量包含到比较的公式中。此外，我们通过比较 Zones域上的扩展技术和Zones与不可比较的Relational Predicates域的比较，对我们的算法进行了实证评估。我们的实证评估结果显示出更好的比较粒度。在比较分析技术时，它减少了较精确的不变量的数量，从而限制了旧有的carry-over效应。此外，它还删除了不可判定的不变量，并减少了在比较两个不可比较的关系抽象域时不可比较的不变量的数量。
作者：Kenny Ballou and Elena Sherman
论文ID：2305.16212
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-05-26