Symmetries occur in different forms in concurrent programs. Such symmetries are induced by processes that behave similarly, and also by data items which are treated similarly by the processes. The talk will present three different methods, based on symmetry reductions, in containing the state explosion problem in model checking. The first method considers the symmetries in the program as well the formula. In this method we first construct a quotient structure, corresponding to the reachable part of the global state graph, and then check the satisfaction of the formula in the quotient structure using the traditional model checking algorithms. This method is primarily useful in checking safety properties. The second method considers only the symmetries in the program and is based on the construction of Annotated Quotient Structure (AQS). The AQS is like the quotient structure excepting that the edges carry additional information. This additional information is used for checking correctness under fairness. This method allows checking of both safety and liveness properties.