量化一阶公式抽象域的高效实现
计算机科学中的逻辑
2024-08-20 v4
摘要
本文为在抽象解释中使用由量化一阶逻辑公式组成的集合构成的抽象域奠定了实用基础。由于涉及公式的复杂性以及抽象元素（即公式集合）的庞大大小，这一抽象域乍看之下似乎不可行。我们引入了抽象元素的高效表示，消除基于一种新型语法子包含关系冗余，该关系近似于语义蕴含。我们开发了算法和数据结构，高效计算抽象元素与具体状态抽象的并集。为证明该域的可行性，我们使用数据结构和算法实现了一种符号抽象算法，计算最佳抽象变换的过渡系统的最小固定点，对应于最强归纳不变式。我们以 Paxos 为例（在我们的表示中包含 个 量化公式），在与最先进的属性导向方法相当的时间内找到了最小固定点。
引用
@article{arxiv.2405.10308,
title = {Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas},
author = {Eden Frenkel and Tej Chajed and Oded Padon and Sharon Shoham},
journal= {arXiv preprint arXiv:2405.10308},
year = {2024}
}