Main Profile

At A Glance

Incremental State-Space Exploration for Programs with Dynamically Allocated Data

Google Tech TalksJune, 4 2008ABSTRACTWe present a novel technique that speeds up state-space exploration(SSE) for evolving programs with dynamically allocated data. SSE isthe essence of explicit-state model checking and an increasinglypopular method for automating test generation. Traditional,non-incremental SSE takes one version of a program and systematicallyexplores the states reachable during the program's executions to ndproperty violations. Incremental SSE considers several versions thatarise during program evolution: reusing the results of SSE for oneversion can speed up SSE for the next version, since state spaces ofconsecutive program versions can have significant similarities. Wehave implemented our technique in two model checkers: Java PathFinderand the J-Sim state-space explorer. The experimental results on 24program evolutions and exploration changes show that for non-initialruns 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 ViswanathanSpeaker: Darko MarinovDarko Marinov is an Assistant Professor in the Department ofComputer Science at the University of Illinois at Urbana-Champaign. Heobtained his Ph.D. from MIT in 2005. His main research interests are inSoftware Engineering, with focus on improving software reliability usingsoftware testing and model checking. His work is supported by NSF andMicrosoft.
Length: 27:47

Contact

Questions about Incremental State-Space Exploration for Programs with Dynamically Allocated Data

Want more info about Incremental State-Space Exploration for Programs with Dynamically Allocated Data? Get free advice from education experts and Noodle community members.

  • Answer

Ask a New Question