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

Abstract

Enter Abstract Here


Notes

Enter Notes Here


BibTeX Reference

@ARTICLE{damorim08TSE, 
title={Delta Execution for Efficient State-Space Exploration of Object-Oriented Programs}, 
author={d'Amorim, M. and Lauterburg, S. and Marinov, D.}, 
journal={Software Engineering, IEEE Transactions on}, 
year={2008}, 
month={Sept.-Oct. }, 
volume={34}, 
number={5}, 
pages={597-613}, 
abstract={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).}, 
keywords={object-oriented programming, program debugging, program testing, program verificationDelta execution, Java programs, automating test generation, model checking, object-oriented programs, sequential Java programs, state-space exploration}, 
doi={10.1109/TSE.2008.37}, 
ISSN={0098-5589}, }
Unless otherwise stated, the content of this page is licensed under Creative Commons Attribution-ShareAlike 3.0 License