Files in this item



application/pdfDelta Execution ... ject-Oriented Programs.pdf (300kB)
(no description provided)PDF


Title:Delta Execution for Efficient State-Space Exploration of Object-Oriented Programs
Author(s):d'Amorim, Marcelo; Lauterburg, Steven; Marinov, Darko
Subject(s):object-oriented programs
computer science
Abstract: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. Previous research has focused on standard program execution that operates on one state/heap. We present Delta Execution, a technique that simultaneously operates on several states/heaps. Delta execution exploits the fact that many execution paths in state-space exploration partially overlap and speeds up the exploration by sharing the common parts across the executions and separately executing only the deltas where the executions differ. The heart of Delta Execution is an efficient representation and manipulation of sets of states/heaps. We have implemented Delta Execution in two model checkers: JPF and BOX. JPF is a popular general-purpose model checker for Java programs, and BOX is a specialized model checker that we have developed for efficient exploration of sequential Java programs. We have evaluated Delta Execution for (bounded) exhaustive exploration of ten basic subject programs without errors. The experimental results show that on average Delta Execution improves the exploration time 10.97x (over an order of magnitude) in JPF and 2.07x in BOX, while taking on average 1.51x less memory in JPF and roughly the same amount of memory in BOX. We have also evaluated Delta Execution for one larger case study with errors, where the exploration time improved up to 1.43x. Additionally, the experimental results for abstract matching, a recently proposed non-exhaustive exploration in JPF, of four subject programs show that on average Delta Execution improves the exploration time 3.37x.
Issue Date:2007-05
Genre:Technical Report
Other Identifier(s):UIUCDCS-R-2007-2844
Rights Information:You are granted permission for the non-commercial reproduction, distribution, display, and performance of this technical report in any format, BUT this permission is only for a period of 45 (forty-five) days from the most recent time that you verified that this technical report is still available from the University of Illinois at Urbana-Champaign Computer Science Department under terms that include this permission. All other rights are reserved by the author(s).
Date Available in IDEALS:2009-04-22

This item appears in the following Collection(s)

Item Statistics