路径可行性查询的实证研究
软件工程
2013-02-21 v1 编程语言
摘要
在本文中，我们对基于路径探索的软件工程方法中生成的路径可行性查询进行了比较研究。基于符号执行的方法在软件工程的各个方面（例如证明程序属性、生成测试用例、比较程序的不同执行）正变得日益重要。这些方法使用 SMT 求解器来检查以支持理论中的公式形式编写的路径可行性查询的可满足性。我们研究了使用 SMT 求解器求解真实世界程序中此类路径可行性查询的性能。我们的路径条件公式是在无量词位向量与数组理论（QF_ABV）中生成的。我们表明，在不同的 SMT 求解器中，STP 在此类查询上的表现比 Z3 好一个数量级。作为应用，我们基于本研究设计了一种新的程序分析（Change Value Analysis），该方法利用了程序中的未定义行为。我们在 LLVM 中实现了该分析，并使用 SIR 程序基准进行了测试。它将求解路径可行性查询所需的时间减少了 48%。本研究可为使用路径可行性查询创建基于符号执行的可扩展软件工程方法的从业者提供指导。
引用
@article{arxiv.1302.4798,
title = {An Empirical Study of Path Feasibility Queries},
author = {Asankhaya Sharma},
journal= {arXiv preprint arXiv:1302.4798},
year = {2013}
}