N. Shah and R. Iranmanesh (Malaysia)
Java PathFinder, JPF, Iterative Deepening Search
Java PathFinder is an explicit-state model checker for Java programs. In search for a given condition, JPF explores all possible execution states that a given program can have, including different possibilities of thread interleavings. Due to large number of possible states and execution paths, JPF performance has been an issue since the beginning. A great amount of work has been in progress to enhance the time and space requirements of JPF model checking. State Generation and Search Algorithms, in particular, play an important role during the execution of JPF. The focus of this paper is to highlight optimality and completeness issues of JPF’s default search algorithm and address it using the well-known Iterative Deepening Search(IDS). Empirical evaluation of Depth First Search(DFS) and Iterative Deepening Search are also presented. From the theoretical point of view, iterative search has better time and space complexity compared to Depth First Search. It is also shown empirically that iterative deepening search can be used to model check programs that are not testable with the default DFS.
Important Links:
Go Back
