Efficient Modular SMT-Based Model Checking of Pointer Programs.

Modularity is indispensable for scaling automatic verification to large programs. However, modularity also introduces challenges because it requires inferring and abstracting the behavior of functions as summaries - formulas that relate the function's inputs and outputs. For programs manipulating memory, summaries must include the function's frame, i.e., how the content memory is affected by the execution of the function. In SMT-based model-checking, memory is often modeled with (unbounded) logical arrays and expressing frames generally requires universally quantified formulas. Such formulas significantly complicate inference and subsequent reasoning and are thus to be avoided. In this paper, we present a technique to encode the memory that is bounded explicitly, eliminating the need for quantified summaries. We build on the insight that the size of frames can be statically known. This enables replacing unbounded arrays with finite maps - a finite collection of key-value pairs. Specifically, we develop a new static analysis to infer the finite parts of a function's frame. We then extend the theory of arrays to the theory of finite maps and show that satisfiability of Constrained Horn Clauses (CHCs) over finite maps is reducible to satisfiability of CHCs over the base theory. Finally, we propose a new encoding from imperative programs to CHCs that uses finite maps to model explicitly the finite memory passed in function calls. The result is a new verification strategy that preserves the advantages of modularity while reducing the need for quantified frames. We have implemented this approach in SEA-HORN, a state-of-the-art CHC-based software model checker for LLVM. An evaluation on Linux Drivers from SV-COMP shows the effectiveness of our technique.