基于候选的归纳不变式生成的实现与评估
软件工程
2017-06-16 v2
摘要
归纳不变式的发现是静态程序验证的核心。目前，许多自动生成归纳不变式的解决方案不够灵活、仅适用于特定类别的程序，或不可预测。在一定程度上规避这些缺陷的一种自动技术是基于候选的归纳不变式生成。本文描述了我们在 GPUVerify（一种针对在 GPU 上运行的程序的静态检查器）中应用基于候选的归纳不变式生成所做的努力。我们研究了一组包含循环的 GPU 程序，这些程序取自多个开源套件和供应商 SDK。我们描述了用于逐步改进 GPUVerify 不变式生成能力以处理这些基准测试的方法，即通过基于候选的归纳不变式生成，利用廉价的静态分析来推测潜在的程序不变式。我们还描述了一组实验，用于检验我们的候选生成规则的有效性，并根据规则的通用性（生成候选不变式的程度）、命中率（生成的候选成立的比例）、价值（可证明的候选实际帮助验证成功的程度）以及影响力（一个生成规则的成功在多大程度上依赖于另一规则生成的候选）来评估规则。GPUVerify 生成的候选帮助验证了 253 个程序中的 231 个。然而，这种精度的提高使 GPUVerify 变得迟缓：生成的候选越多，确定哪些是归纳不变式所花费的时间就越多。为了加速这一过程，我们研究了四种欠近似程序分析，旨在快速拒绝错误的候选，以及一个使这些分析可以串行或并行运行的框架。
引用
@article{arxiv.1612.01198,
title = {Implementing and Evaluating Candidate-Based Invariant Generation},
author = {Adam Betts and Nathan Chong and Pantazis Deligiannis and Alastair F. Donaldson and Jeroen Ketema},
journal= {arXiv preprint arXiv:1612.01198},
year = {2017}
}