基于摘要引导搜索的软件模型检测

《Proceedings of the ACM on Programming Languages》：Software Model Checking via Summary-Guided Search

GPS是一种基于静态分析的软件模型检查算法，通过路径剪枝和测试生成高效发现程序错误，采用双层搜索策略优化长路径错误检测，并引入动态补全技术保持性能，在多个基准测试中表现优于现有工具。

　　

摘要

在这项工作中，我们描述了一种名为GPS的新软件模型检测算法。GPS将程序的模型检测任务视为对程序状态的定向搜索，这一搜索过程由基于组合原理的静态分析指导。静态分析生成的摘要不仅用于剔除不可行的路径，还用于驱动测试生成，以探索新的、未被覆盖的程序状态。GPS能够找到证明程序安全性的证据，也能找到证明程序不安全的反例（即能够触发错误的输入）。该算法采用了一种新颖的双层搜索策略，使其在检测具有较长、依赖于输入的错误路径的程序中的错误时尤为高效。为了使GPS具备反驳完备性（即如果在给定足够时间的情况下存在错误，GPS能够找到该错误），我们引入了一种仪器化技术，并证明了这种技术可以在不牺牲整体性能的情况下帮助GPS实现反驳完备性。我们在一系列基准测试中对GPS进行了评估，这些基准测试包括来自软件验证竞赛（SV-COMP）的程序、现有文献中的程序，以及基于本文示例生成的合成程序。结果表明，我们的GPS实现不仅在解决的基准测试数量上，而且在运行时间方面，都优于现有的最先进软件模型检测器（包括SV-COMP ReachSafety-Loops类别中的最佳算法）。