On the non-termination of MDG-based abstract state enumeration

Multiway decision graphs are a new class of decision graphs for representing abstract states machines. This yields a new verification technique that can deal with the data-width problem by using abstract sorts and uninterpreted functions to represent data value and data operations, respectively. However, in many cases, it may suffer from the non-termination of the state enumeration procedure. This paper presents a novel approach to solving the non-termination problem when the generated set of states, even infinite, represents a structured domain where terms (states) share certain repetitive patterns. The approach is based on the schematization method developed by Chen and Hsiang, namely rho-terms. Schematization provides a suitable formalism for finitely manipulating infinite sets of terms. We illustrate the effectiveness of our method by several examples. (C) 2002 Elsevier Science B.V. All rights reserved.