基于PDR的软件验证：前沿技术的实现与实证评估
软件工程
2020-02-25 v2
摘要
性质导向可达性(PDR)是一种基于SAT/SMT的可达性算法，可增量式构造归纳不变量。在成功应用于硬件模型检验后，已有若干面向软件模型检验的改造方案被提出。我们贡献了一项可复现且详尽的当前最优技术对比评估：我们(1)实现了独立的PDR算法，并作为改进，实现了一种用于k-归纳的基于PDR的辅助不变量生成器；(2)在最大的公开可用C验证任务基准集上进行了实验研究，探索了基于PDR的软件验证的有效性与效率。我们工作的主要贡献是通过提供良好工程的参考实现和现有技术的实验评估，为该地区持续研究建立可复现的基线。
引用
@article{arxiv.1908.06271,
title = {Software Verification with PDR: Implementation and Empirical Evaluation of the State of the Art},
author = {Dirk Beyer and Matthias Dangl},
journal= {arXiv preprint arXiv:1908.06271},
year = {2020}
}
备注
35 pages, 8 tables, 13 figures, supplementary web page: https://www.sosy-lab.org/research/pdr-compare/, replication package: https://doi.org/10.5281/zenodo.3370037