Automated generation of model classes for Java PathFinder

Model checkers like Java PathFinder (JPF) often have to combat the state space explosion problem. One solution adopted to tackle this problem is to abstract away parts of the system, e. g., to model complex library classes at a higher level of abstraction. The model classes have the same interface as the actual library classes but exhibit reduced be- haviour and state. Writing such model classes is both error prone and time consuming. In this paper we propose a tool that can automatically derive a model class from the original class. To achieve this goal, the tool uses different algorithms, including slicing and value generation, each yielding a model class with different behaviour and state.