  In a previous paper we have presented a CEGAR approach for the verification
of parameterized systems with an arbitrary number of processes organized in an
array or a ring. The technique is based on the iterative computation of
parameterized invariants, i.e., infinite families of invariants for the
infinitely many instances of the system. Safety properties are proved by
checking that every global configuration of the system satisfying all
parameterized invariants also satisfies the property; we have shown that this
check can be reduced to the satisfiability problem for Monadic Second Order on
words, which is decidable.
  A strong limitation of the approach is that processes can only have a fixed
number of variables with a fixed finite range. In particular, they cannot use
variables with range [0,N-1], where N is the number of processes, which appear
in many standard distributed algorithms. In this paper, we extend our technique
to this case. While conducting the check whether a safety property is inductive
assuming a computed set of invariants becomes undecidable, we show how to
reduce it to checking satisfiability of a first-order formula. We report on
experiments showing that automatic first-order theorem provers can still
perform this check for a collection of non-trivial examples. Additionally, we
can give small sets of readable invariants for these checks.
