Software Model Checking via Summary-Guided Search (Extended Version)

TL;DR

This paper introduces GPS, a novel software model-checking algorithm that uses summary-guided search and static analysis to efficiently verify program safety and find bugs, outperforming existing tools.

Contribution

The paper presents GPS, a new model-checking approach combining summary-based static analysis with a two-layered search strategy for improved bug detection and proof of safety.

Findings

GPS outperforms state-of-the-art model checkers in benchmarks

GPS effectively finds bugs in long, input-dependent error paths

GPS achieves refutation-completeness with an innovative instrumentation technique

Abstract

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.