We will give an overview of our work during the last year on model checking of parameterized systems.A parameterized systems consists of an arbitrary number of components. The task is to perform parameterized verification, i.e., to verify correctness of the system regardless of the number of components. Examples of parameterized systems include mutual exclusion protocols, cache coherence protocols, and multi-threaded programs.We start by describing an efficient method to prove safety properties for a simple class of parameterized systems, namely those which have linear topologies and where each process is a finite-state automaton. A main feature is that we allow transitions that are guarded by global conditions where a component may ask about the states of all the other components inside the system.The method derives an over-approximation of the induced transition system, which allows the use of a simple class of regular expressions as a symbolic representation for infinite sets of states. Compared to traditional regular model checking methods, the analysis does not require the manipulation of transducers, and hence its simplicity and efficiency.We will describe how to extend the method to handle more intricate features, such as having infinite-state processes, non-atomic global conditions, and tree- or graph-like topologies.We have implemented a prototype which works well on several complicated mutual exclusion algorithms and cache coherence protocols.