超越 k-归纳：从反例学习以双向探索状态空间
计算机科学中的逻辑
2019-04-05 v1
摘要
我们描述并评估了一种称为双向 k-归纳（bkind）的新颖 k-归纳证明规则，其显著提升了 k-归纳的缺陷发现能力。特别地，bkind 利用过近似步骤生成的 counterexamples（反例）推导新性质并反馈给有界模型检验过程。我们还将区间不变式生成器与 bkind 结合，以显著提升正确验证结果的数量。实验结果表明，与朴素 k-归纳证明规则相比，bkind 可大幅减少验证时间，因为它仅需一半步数即可在不安全程序中找到给定的安全性质违例。bkind 算法优于另一最先进的 k-归纳验证器 2LS，并且在分析大量公开可用基准时，产生的正确证明多于两倍，正确报警约多 35%。
引用
@article{arxiv.1904.02501,
title = {Beyond k-induction: Learning from Counterexamples to Bidirectionally Explore the State Space},
author = {Mikhail R. Gadelha and Felipe R. Monteiro and Enrico Steffinlongo and Lucas C. Cordeiro and Denis A. Nicole},
journal= {arXiv preprint arXiv:1904.02501},
year = {2019}
}
备注
17 pages