Incremental state-space exploration for programs with dynamically allocated data

We present a novel technique that speeds up state-space exploration (SSE) for evolving programs with dynamically allocated data. SSE is the essence of explicit-state model checking and an increasingly popular method for automating test generation. Traditional, non-incremental SSE takes one version of a program and systematically explores the states reachable during the program's executions to nd property violations. Incremental SSE considers several versions that arise during program evolution: reusing the results of SSE for one version can speed up SSE for the next version, since state spaces of consecutive program versions can have sig-ni cant similarities. We have implemented our technique in two model checkers: Java PathFinder and the J-Sim state-space explorer. The experimental results on 24 program evolutions and exploration changes show that for non-initial runs our technique speeds up SSE in 22 cases from 6.43% to 68.62 % (with median of 42.29%) and slows down SSE in only two cases for-4.71 % and-4.81%