关于PDR中证明义务泛化的所有疑问
计算机科学中的逻辑
2022-08-19 v4
摘要
本文重新审视位级性质定向可达性（PDR）中证明义务泛化这一主题。我们提供了全面的研究，其（1）确定了该问题的复杂度，（2）深入分析了现有方法的局限性，（3）引入了从未在PDR背景下使用过的证明义务泛化方法，（4）从理论角度比较了不同方法的优势，以及（5）在硬件模型检验和AI规划的各种基准上对这些方法进行了密集评估。
引用
@article{arxiv.2105.09169,
title = {Everything You Always Wanted to Know About Generalization of Proof Obligations in PDR},
author = {Tobias Seufert and Felix Winterer and Christoph Scholl and Karsten Scheibler and Tobias Paxian and Bernd Becker},
journal= {arXiv preprint arXiv:2105.09169},
year = {2022}
}