Constraint-Based model checking of data-independent systems

Data-independent systems are an important class of infinite-state systems which can be subject to model checking by first building finite-state property-preserving abstractions. Exploiting data independence in practice involves user guidance, either in terms of the abstraction itself or in terms of symmetry properties of the system. In this paper we present a constraint-based verification technique that automatically handles data-independent systems. Our technique introduces a unified, automata-based model for infinite-state systems and LTL formulas. The technique can be seen as a generalization of explicit state model checker for reachability and LTL properties. We have implemented our technique using logic programming with tabulation and constraints. We also describe an extension to the automata model that permits verification of a richer class of systems. We show its power by analyzing configuration (security) vulnerabilities in a computer system.