Space-Reduction Strategies for Model Checking Dynamic Software

Abstract

Effective model-checking of modern object-oriented software systems requires providing support for program features such as dynamically created threads, heap-allocated objects and garbage collection. These features have often proven problematic to treat using many previous model-checking frameworks that do not provide sophisticated heap representations and optimizations. In this paper, we define a flexible framework for combined heap and thread symmetry reductions in explicit-state model checking that can be tuned to trade run-time overhead for precision. In addition, we describe various strategies for duplication-reducing state-space encodings for object-oriented heap structures. We have implemented these techniques in Bogor (our extensible software model-checking framework), and we present empirical data to support the effectiveness of these memory reductions on a collection of realistic examples and to demonstrate that they improve upon previous approaches. These techniques, formalized in a group theoretic framework, can be applied to any non-deterministic heap object diagram.