Keywords

verification, validation, guided search, model checking, structural heuristics

Abstract

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.

Original Publication Citation

N. Rungta and E. G. Mercer, "A Context-sensitive Structural Heuristic for Guided Search Model Checking", in Proceedings of 2th IEEE/ACM International Conference on Automated Software Engineering, Long Beach, USA, pages 41-413, November 25.