Incremental state-space exploration for programs with dynamically allocated data

Steven Lauterburg, Ahmed Sobeih, Darko Marinov, Mahesh Viswanathan

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 find 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%.

Original languageEnglish (US)
Title of host publicationICSE'08
Subtitle of host publicationProceedings of the 30th International Conference on Software Engineering 2008
Pages291-300
Number of pages10
DOIs
StatePublished - 2008
Event30th International Conference on Software Engineering 2008, ICSE'08 - Leipzig, Germany
Duration: May 10 2008May 18 2008

Publication series

NameProceedings - International Conference on Software Engineering
ISSN (Print)0270-5257

Other

Other30th International Conference on Software Engineering 2008, ICSE'08
Country/TerritoryGermany
CityLeipzig
Period5/10/085/18/08

Keywords

  • Incremental computation
  • J-Sim
  • JPF
  • Java PathFinder
  • State-space exploration
  • model checking

ASJC Scopus subject areas

  • Software

Fingerprint

Dive into the research topics of 'Incremental state-space exploration for programs with dynamically allocated data'. Together they form a unique fingerprint.

Cite this