Delta Execution for Efficient State-Space Exploration of Object-Oriented Programs

We present Delta Execution, a technique that speeds up state-space exploration of object-oriented programs. Statespace exploration is the essence of model checking and an increasingly popular approach for automating test generation. A key issue in exploration of object-oriented programs is handling the program state, in particular the heap. We exploit the fact that many execution paths in state-space exploration partially overlap. Delta Execution simultaneously operates on several states/heaps and shares the common parts across the executions, separately executing only the "deltas" where the executions differ. We implemented Delta Execution in two model checkers: JPF, a popular general-purpose model checker for Java programs, and BOX, a specialized model checker that we developed for efficient exploration of sequential Java programs. The results for bounded-exhaustive exploration of ten basic subject programs and one larger case study show that Delta Execution reduces

• Type: Journal
• Year: 2008
• Where: TSE
• Authors: Marcelo d'Amorim, Steven Lauterburg, Darko Marinov
• Keywords: Delta Execution, Exploration, State-space Exploration, TSE 2008