A uniform constraint-based framework for the verification of infinite state systems

Abstract

Automatic verification of infinite state systems is an important area of research. Unlike its finite state counterpart, in spite of the existence of a large body of theoretical and practical results on automatic verification of infinite state systems, there does not exist a uniform framework that is applicable to a large class of systems and that facilitates description of procedures that solves the verification problem for infinite state systems in practice as well as providing tools for reasoning about the termination conditions of such procedures. The purpose of this dissertation is to provide a uniform framework that (1) allows description of infinite state systems at their own level of granularity, (2) allows specifying their properties at a high level, (3) allows description of procedures, that can solve in practice the verification problems for infinite state systems, in a declarative fashion, (4) provides tools to reason about the termination conditions for such procedures, (5) facilitates derivation of abstractions for verification as well as easy incorporation of optimization techniques, (6) allows clear separation of the logical aspects of verification from the combinatorial ones, (7) allows combination of deductive (proof-theoretic) methods with model-theoretic ones and (8) provides, for free, data structures for implicit representation of possibly infinite sets of states.