Space-Reduction Strategies for Model Checking Dynamic Software |
| |
Authors: | Robby Matthew B Dwyer John Hatcliff Radu Iosif |
| |
Affiliation: | aDepartment of Computing and Information Sciences, Kansas State University 234 Nichols Hall, Manhattan KS, 66506, USA;bVerimag/CNRS 2 Avenue de Vignate, 38610 Gieres, France |
| |
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. |
| |
Keywords: | |
本文献已被 ScienceDirect 等数据库收录! |
|