To obtain scalability, software model checkers often employ modular analysis techniques that analyze each of the procedures in a program separately. In this context, summaries are used to abstract the behavior of procedures, as relations of their input/output parameters, to analyze any procedure call without inlining or analyzing its body. One key challenge when producing summaries of memory-manipulating programs is to solve the frame problem: determining which memory locations are not changed by a procedure.

In SMT-based model checking, the program heap is usually modeled by logical (unbounded) arrays. A pointer analysis is typically used as a pre-analysis to divide the heap into multiple disjoint regions, such that each region is encoded into an array. In general, a summary contains two arrays (input and output) per memory region, describing all possible values before and after the call to the procedure. A naive SMT encoding requires quantifiers to express which elements of the output array are equal to the input array. Although some SMT solvers can handle formulas with quantifiers, the problem is in general undecidable and, therefore, we want to avoid them if possible.

In this talk we will show how to leverage a pointer analysis to produce an SMT encoding that enforces the SMT solver to search only for quantifier-free summaries. First, we use the explicit heap representation that the pointer analysis produces to distinguish between finite and potentially infinite memory regions accessed by a procedure. Second, we introduce a new SMT encoding that replaces array variables with scalars if the procedure only uses a finite amount of memory.

This is a joint work with Jorge Navas and Arie Gurfinkel.