一句话：提出 GPS：用组合摘要静态分析引导程序状态有向搜索，高效证明安全并发现反例。
软件模型检测需同时给出安全性证明与反例，但长且依赖输入的错误路径往往难以高效发现。本文提出 GPS 算法，将模型检测视为程序状态空间中的有向搜索，并由基于组合摘要的静态分析引导：摘要既用于剪除不可行路径，也驱动测试生成以探索新状态；同时设计两层搜索策略，并引入 instrumentation 技术使算法达到反驳完备性（给定足够时间必能发现已有错误）而不显著牺牲性能。作者在 SV-COMP、既有文献与合成程序等多样化基准上评估 GPS，结果显示其在求解基准数量和运行时间上均优于最先进的软件模型检测器，包括 SV-COMP ReachSafety-Loops 类别的顶尖工具。
In this work, we describe a new software model-checking algorithm called GPS. GPS treats the task of model checking a program as a directed search of the program states, guided by a compositional, summary-based static analysis. The summaries produced by static analysis are used both to prune away infeasible paths and to drive test generation to reach new, unexplored program states. GPS can find both proofs of safety and counter-examples to safety (i.e., inputs that trigger bugs), and features a novel two-layered search strategy that renders it particularly efficient at finding bugs in programs featuring long, input-dependent error paths. To make GPS refutationally complete (in the sense that it will find an error if one exists, if it is allotted enough time), we introduce an instrumentation technique and show that it helps GPS achieve refutation-completeness without sacrificing overall performance. We benchmarked GPS on a diverse suite of benchmarks including programs from the Software Verification Competition (SV-COMP), from prior literature, as well as synthetic programs based on examples in this paper. We found that our implementation of GPS outperforms state-of-the-art software model checkers (including the top performers in SV-COMP ReachSafety-Loops category), both in terms of the number of benchmarks solved and in terms of running time.
@article{paperbot2991,
title = {Software Model Checking via Summary-Guided Search},
author = {Ruijie Fang and Zachary Kincaid and Thomas Reps},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763142}
}