Deciding Assertions in Programs With References

We present a model checking algorithm for deciding assertions in programs with references. Our algorithm is precise, and terminates on programs with finite base types and non-recursive reference types. Non-recursive reference types do not imply a bound on the heap size. Therefore, our algorithm terminates and yields precise results even on programs that allocate unbounded amount of memory, as long as the base types are finite and reference types are non-recursive. Thus, we can extend Boolean Programs to include non-recursive references, and still use a model checker to decide assertions. We have implemented this algorithm in the zing model checker, which supports a rich input language with references as well as concurrent threads. Even though termination is guaranteed only for programs with finite base types and non-recursive reference types, in practice, the algorithm terminates for several programs which do not satisfy these restrictions, and improves the peformance of the model checker. Our algorithm improved the performance of the model checker by 30-35% on a concurrent transaction management program with 7000 lines of code, 57 dynamic allocation sites, and several million reachable states and found a subtle concurrency bug.