面向 k-归纳的分层认证
计算机科学中的逻辑
2022-08-03 v1
摘要
我们近期提出的基于位级 k-归纳模型检测的认证框架，已被证明在提升验证结果可信度方面相当有效，尽管其部分涉及量词推理。在本文中，我们展示如何通过假设复位函数是分层的来简化该方法。这样它可以被提升到字级，原则上也可用于量词推理困难的其它理论。我们的新方法需要六次简单 SAT 检查和一次多项式时间检查，使得认证保持在 co-NP 内，而此前的方法需要五次 SAT 检查和一次 QBF 检查。实验结果显示我们的新方法在性能上有显著提升。最后，我们展示并评估了新工具 Certifaiger-wl，其能够对基于 k-归纳的字级模型检查进行认证。
引用
@article{arxiv.2208.01443,
title = {Stratified Certification for k-Induction},
author = {Emily Yu and Nils Froleyks and Armin Biere and Keijo Heljanko},
journal= {arXiv preprint arXiv:2208.01443},
year = {2022}
}