We present a new abstract interpretation framework for the precise over-approximation of numerical fixpoint iterators. Our key observation is that unlike in standard abstract interpretation (AI), typically used to over-approximate all reachable program states, in this setting, one only needs to abstract the concrete fixpoints, i.e., the final program states. Our framework targets numerical fixpoint iterators with convergence and uniqueness guarantees in the concrete and is based on two major technical contributions: (i) theoretical insights which allow us to compute sound and precise fixpoint abstractions without using joins, and (ii) a new abstract domain, CH-Zonotope, which admits efficient propagation and inclusion checks while retaining high precision. We implement our framework in a tool called CRAFT and evaluate it on a novel fixpoint-based neural network architecture (monDEQ) that is particularly challenging to verify. Our extensive evaluation demonstrates that CRAFT exceeds the state-of-the-art performance in terms of speed (two orders of magnitude), scalability (one order of magnitude), and precision (25% higher certified accuracies).

翻译：我们提出了一种新的抽象解释框架，用于对数值型不动点迭代器进行精确的过近似。我们的关键观察在于，与标准抽象解释（AI）通常用于过近似所有可达程序状态不同，在此场景下只需抽象具体的不动点，即程序的最终状态。该框架针对在具体域中具有收敛性和唯一性保证的数值型不动点迭代器，基于两大技术贡献：（i）理论洞见，使我们能够在无需使用联接操作的情况下计算可靠且精确的不动点抽象；（ii）新抽象域CH-Zonotope，它在保持高精度的同时支持高效的传播和包含性检查。我们将该框架实现为工具CRAFT，并在一种特别难以验证的新型基于不动点的神经网络架构（monDEQ）上进行了评估。大量实验表明，CRAFT在速度（两个数量级）、可扩展性（一个数量级）和精度（认证准确率提升25%）方面均超越了现有最优性能。