IC3泛化中的引理预测
软件工程
2024-11-21 v1
摘要
IC3算法（也称为PDR）因其高效性、可扩展性和完备性，近年来在安全模型检测领域产生了重大影响。IC3最关键的组成部分是归纳泛化，它涉及逐一丢弃变量，且通常是最耗时的步骤。在本文中，我们提出了一种新方法，利用反例传播在丢弃变量之前预测可能的最小引理。通过利用这种方法，如果预测成功，我们可以避免丢弃变量。综合评估表明，引理预测取得了令人称赞的成功率，并且我们提出的方法实现了显著的性能提升。
引用
@article{arxiv.2411.12749,
title = {Predicting Lemmas in Generalization of IC3},
author = {Yuheng Su and Qiusong Yang and Yiwei Ci},
journal= {arXiv preprint arXiv:2411.12749},
year = {2024}
}