基于局部策略迭代的程序分析
计算机科学中的逻辑
2016-04-20 v3 编程语言
摘要
我们提出一种用于推导数值不变量的新算法，它结合了最大策略迭代(max-policy iteration)的精度与传统Kleene迭代的灵活性和可扩展性。该算法定义于可配置程序分析(Configurable Program Analysis, CPA)框架中，从而允许分析间通信。它使用可调块编码(adjustable-block encoding)以遍历可能包含分支的无循环程序段，而不引入额外抽象。我们的技术作用于任何模板线性约束域，包括区间域和八边形域；模板也可从程序源代码导出。该实现在来自软件验证竞赛(Software Verification Competition, SV-Comp)的一组基准测试上进行了评估。它与最先进的的分析器相比具有竞争力。
引用
@article{arxiv.1509.03424,
title = {Program Analysis with Local Policy Iteration},
author = {George Karpenkov and David Monniaux and Philipp Wendler},
journal= {arXiv preprint arXiv:1509.03424},
year = {2016}
}