Issue No. 05 - Sept.-Oct. (2008 vol. 34)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TSE.2008.37
Marcelo d'Amorim , University of Illinois at Urbana-Champaign, Urbana
Steven Lauterburg , University of Illinois at Urbana-Champaign, Urbana
Darko Marinov , University of Illinois at Urbana-Champaign, Urbana
We present Delta Execution, a technique that speeds up state-space exploration of object-oriented programs. State-space 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 exploration time from 1.06x to 126.80x (with median 5.60x) in JPF and from 0.58x to 4.16x (with median 2.23x) in BOX. The results for a non-exhaustive exploration in JPF show that Delta Execution reduces exploration time from 0.92x to 6.28x (with median 4.52x).
Software/Program Verification, Model checking, Testing and Debugging
Marcelo d'Amorim, Steven Lauterburg, Darko Marinov, "Delta Execution for Efficient State-Space Exploration of Object-Oriented Programs", IEEE Transactions on Software Engineering, vol. 34, no. , pp. 597-613, Sept.-Oct. 2008, doi:10.1109/TSE.2008.37