Scifaro

中文

用于基于学习的无量词循环不变式推断的谓词生成

计算机科学中的逻辑 2015-07-01 v2 机器学习

作者: Wonchan Lee , Yungbum Jung , Bow-yaw Wang , Kwangkuen Yi

在 arXiv 上查看 ↗ PDF ↗ DOI ↗

摘要

我们解决了循环不变式推断背景下的谓词生成问题。受基于插值的抽象细化技术启发，我们应用插值定理来合成由程序文本隐含的谓词。我们的技术能够提高文献 [14] 中基于学习的循环不变式推断算法的有效性和效率。我们报告了来自 Linux、SPEC2000 和 Tar 实用程序的示例的实验结果。

关键词

谓词生成循环不变式推断插值定理抽象细化基于学习的算法程序验证

引用

@article{arxiv.1207.7167,
  title  = {Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference},
  author = {Wonchan Lee and Yungbum Jung and Bow-yaw Wang and Kwangkuen Yi},
  journal= {arXiv preprint arXiv:1207.7167},
  year   = {2015}
}