按需量词
计算机科学中的逻辑
2021-06-02 v1 编程语言
摘要
自动程序验证是一个困难问题。即便对于线性整数算术（LIA）上的转移系统，它也是不可判定的。将转移系统扩展至数组理论，会因需要借助全称量化公式进行推断与推理而进一步使问题复杂化。本文提出一种新算法 Quic3，它将 IC3 扩展以推断 LIA 与数组联合理论上的全称量化不变式。不同于其他将 IC3 或 SMT 求解器用作黑箱的方法，Quic3 精心管理量化泛化（以构造量化不变式）与量词实例化（以在存在量词时检测收敛）。尽管 Quic3 不保证收敛，但它保证通过探索越来越长的执行路径来取得进展。我们已在 Z3 的约束 Horn 子句求解引擎中实现了 Quic3，并通过将其应用于验证各类公开基准的数组操作 C 程序进行了实验。
引用
@article{arxiv.2106.00664,
title = {Quantifiers on Demand},
author = {Arie Gurfinkel and Sharon Shoham and Yakir Vizel},
journal= {arXiv preprint arXiv:2106.00664},
year = {2021}
}