Software Model Checking with Path and Procedure Summaries

Abstract

“If debugging is the process of removing bugs, then programming must be the process of putting them in.” —Edsgar W. Dijkstra.

Perhaps as a corollary to the Dijkstra quote above, folk wisdom has it that finding bugs is easy in comparison to proving program safety. As such, a theme central to the software model checking literature over the past decade has been the development of sophisticated refinement techniques to prove program safety. In other words, establishing good over-approximations of program dynamics that lead to safety proofs is a nontrivial task. In this thesis, we investigate the design of a software model checking algorithm, using the opposite version of the aforementioned insight: Our algorithm leverages algebraic program analysis (APA), a recent static analysis technique that formulates the problem of statically analyzing program properties as solving algebraic path problems in the control flow graph. An APA-based reachability analysis produces precise over-approximate path and procedure summaries, which often render the task of proving program safety easy — in contrast to prior work. Leveraging this insight, our algorithm focuses on establishing concrete execution traces that lead to assertion violations (i.e. bug-finding), while retaining refinement abilities that are further aided by summaries produced by algebraic program analysis. Our resultant algorithm, GPS, is capable of analyzing sequential programs with recursive procedure calls. The features of our model checking algorithm that distinguishes it from previous literature are 1) the algebraic presentation of the model checking algorithm, leveraging both overapproximate summaries produced by algebraic program analysis, interpolation, and concolic execution; 2) a new technique, which we call extrapolation, used to perform compositional, interprocedural concolic execution, with a definition being the syntactic dual of interpolation. We evaluate the performance of GPS on a subset of Software Verification Competition (SV-COMP) benchmarks and show that it is competitive with state-of-the-art.