PAGAI：一种路径敏感的静态分析器
编程语言
2012-07-18 v1 计算机科学中的逻辑
摘要
我们描述了 PAGAI 的设计与实现，这是一种基于 LLVM 编译器基础设施的新型静态分析器，用于计算被分析程序数值变量的归纳不变式。PAGAI 实现了多种结合抽象解释与判定过程（SMT 求解）的最先进算法，侧重于区分控制流图内的路径，同时避免系统性的指数级枚举。该工具在所使用的抽象域、迭代算法和判定过程方面具有参数化特性。我们在个人基准测试和广泛可用的 GNU 程序上进行了大量实验，比较了各种分析算法与抽象域组合的时间效率与精度。
引用
@article{arxiv.1207.3937,
title = {PAGAI: a path sensitive static analyzer},
author = {Julien Henry and David Monniaux and Matthieu Moy},
journal= {arXiv preprint arXiv:1207.3937},
year = {2012}
}
备注
Tools for Automatic Program AnalysiS (TAPAS 2012), Deauville : France (2012)