抽象解释中的升序和降序阶段解耦
摘要：抽象解释以仿真具体程序在抽象域$mathbb{A}$上的固定点计算来近似程序的语义。抽象的（后）固定点计算经典地分为两个阶段：上升阶段使用扩展算子作为外推算子来强制终止，随后是下降阶段使用收敛算子来插值，以减小扩展算子引入的精度损失的影响。在本文中，我们提出了一种简单的变体，以更有效地恢复精度，将这两个阶段解耦：特别是，在开始下降阶段之前，我们用更准确的抽象域$mathbb{D}$替换抽象域$mathbb{A}$。这种方法的正确性通过将其视为A$^2$I框架的一个实例来证明。在演示了该新技术在一个简单示例上的效果后，我们总结了初步实验评估的结果，表明它能够在多种抽象域$mathbb{A}$和$mathbb{D}$的选择中获得显著的精度提升。
作者：Vincenzo Arceri and Isabella Mastroeni and Enea Zaffanella
论文ID：2206.10893
分类：Programming Languages
分类简称：cs.PL
提交时间：2022-06-23