A context-sensitive structural heuristic for guided search model checking

Software verification using model checking often translates programs into corresponding transition systems that model the program behavior. As software systems continue to grow in complexity and size, exhaustively checking a property on a transition graph becomes difficult. The goal of guided search heuristics in model checking is to find a counterexample to the property being verified as quickly as possible in the transition graph. The FSM distance heuristic builds an interprocedural control flow graph of the program to estimate distance to a possible error state. It ignores calling context and underestimates the true distance to the error. 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 ac...

• Type: Conference
• Year: 2005
• Where: KBSE
• Authors: Neha Rungta, Eric G. Mercer
• Keywords: FSM Distance, Heuristic, KBSE 2005, Model Checking, Software Engineering