In this paper we build on the FSM distance heuristic for guided model checking by using the runtime stack to reconstruct calling context in procedural calls. We first build a more accurate static representation of the program by including a bounded level of calling context. We then use the calling context in the runtime stack with the more accurate control flow graph to estimate the distance to the possible error state. The heuristic is computed using both the dynamic and static construction of the program. We evaluate the new heuristic on models with concurrency errors. In these examples, experimental results show that for programs with function calls, the new heuristic better guides the search toward the error while the traditional FSM distance heuristic degenerates into a random search.

Pdf version

Poster

N. Rungta and E. G. Mercer. “A Context-sensitive Structural Heuristic for Guided Search Model Checking,” 20th IEEE/ACM International Conference on Automated Software Engineering, Long Beach, USA, November 2005.

 @InProceedings{rungta:ase05,
 author =   {N. Rungta and E. G. Mercer},
 title =   {A Context-Sensitive Structural Heuristic for Guided Search Model Checking},
 booktitle =  {20th IEEE/ACM International Conference on Automated Software Engineering},
 year =  {2005},
 address =  {Long Beach, California, USA},
 month =  {November},
 OPTorganization = {},
 publisher =  {},
 OPTnote =   {},
 pages = {410--413},
 }