The paper presents a method, called the method of VERIFICATION
BY INVISIBLE INVARIANTS for the automatic verification of a large
classes of parameterized systems. The method is based on the automatic
calculation of candidate inductive assertions and checking for their
inductiveness, using symbolic model-checking techniques for both
tasks. First, we show how to use model-checking techniques over finite
(and small) instances of the parameterized system in order to derive
candidates for invariant assertions. Next, we show that the premises
of the standard deductive INV rule for proving invariance
properties can be automatically resolved by finite-state
BDD-based methods with no need for interactive theorem proving.
Combining the automatic computation of invariants with the automatic
resolution of the VCs (verification conditions) yields a (necessarily)
incomplete but fully automatic sound method for verifying large classes
of parameterized systems. The generated invariants can be transferred
to the VC-validation phase without ever been examined by the user,
which explains why we refer to them as ``invisible''.
The paper extends a previous presentation of this method in TACAS'01
by allowing inequality comparisons between variables and parameterized
arrays whose values range over parameterized domains. The efficacy of
the method is demonstrated by automatic verification of diverse
parameterized systems.
