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.

Full Paper and Presentation


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.


 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},

vv-lab/a-context-sensitive-structural-heuristic-for-guided-search-model-checking.txt · Last modified: 2015/02/18 12:55 by egm
Back to top
CC Attribution-Share Alike 4.0 International
chimeric.de = chi`s home Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0