Sciweavers

Share
TSE
2008

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

9 years 7 months ago
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
Marcelo d'Amorim, Steven Lauterburg, Darko Marinov
Added 15 Dec 2010
Updated 15 Dec 2010
Type Journal
Year 2008
Where TSE
Authors Marcelo d'Amorim, Steven Lauterburg, Darko Marinov
Comments (0)
books