Incremental State-Space Exploration for Programs with Dynamically Allocated Data
5Google Tech Talks
June, 4 2008
ABSTRACT
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 significant 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%.
Joint work with Steven Lauterburg, Ahmed Sobeih, and Mahesh Viswanathan
Speaker: Darko Marinov
Darko Marinov is an Assistant Professor in the Department of
Computer Science at the University of Illinois at Urbana-Champaign. He
obtained his Ph.D. from MIT in 2005. His main research interests are in
Software Engineering, with focus on improving software reliability using
software testing and model checking. His work is supported by NSF and
Microsoft.