Addressing Dynamic Issues of Program Model Checking

Abstract. Model checking real programs has recently become an active research area. Programs however exhibit two characteristics that make model checking di cult: the complexity of their state and the dynamic nature of many programs. Here we address both these issues within the context of the Java PathFinder (JPF) model checker. Firstly, we will show how the state of a Java program can be encoded e ciently and how this encoding can be exploited to improve model checking. Next we show how to use symmetry reductions to alleviate some of the problems introduced by the dynamic nature of Java programs. Lastly, we show how distributed model checking of a dynamic program can be achieved, and furthermore, how dynamic partitions of the state space can improve model checking. We support all our ndings with results from applying these techniques within the JPF model checker.

• Type: Conference
• Year: 2001
• Where: SPIN
• Authors: Flavio Lerda, Willem Visser
• Keywords: Dynamic Nature, Model Checker, Model Checking, SPIN 2001, Theoretical Computer Science