The papers [PRZ01] and [APR+01] consider verification of parametrized systems through invariant (induction) based proofs. A major challenge here is to invent induction hypotheses which are sufficiently powerful to verify the given property. The papers describe a method where finite state model checking is used both deriving candidates induction assertions, and to prove that the candidate assertions are indeed inductive. Both steps are performed automatically without the use of theorem provers. The efficiency of the method is demonstrated through verification of several types of parametrized systems such as mutual exclusion protocols and cache coherence protocols.