The high speed requirements on today's processors can be met by pipeline architectures. But pipeline structures cause hazards which is their main drawback. In principle there are two ways to handle hazards: the compiler avoids hazard-causing code sequences or the hardware treats the hazard situations.The compiler-based method has the advantage that extra hardware is not needed whereas the implementation in hardware allows a higher performance. One way to find a satisfying solution is the combination of both ideas: Some of the hazards are handled by the hardware while the remaining hazard-causing code sequences are avoided by the compiler.Using this approach it is possible to move the treatment of hazards from software to hardware and vice versa until a good compromise between small hardware (low power consumption) and sufficient performance has been found. Such solutions are important for mobile systems.To support such an optimization and to ensure that all hazards are taken into account one can derive all hazard-causing code sequences from the hardware description (e.g. RTL model) of the processor. Then a compiler that exclude all these code sequences can be built and a performance evaluation is carried out. The definition of the hazard treatment on-chip, the derivation of the hazard-causing code sequences, and the performance evaluation have to be repeated until the speed and size constrains are fulfilled.In this work we propose a method which allows the computation of all code sequences that cause control hazards. Our method can be divided into two steps.First we model the relevant behavior of the processor as a finite state machine (FSM). The modeling is carried out by an abstraction of the behavioral description of the processor which preserves the properties that are relevant for the hazard checking.In the second step we determine the hazard-causing code sequences by applying symbolic model checking. In contrast to other model checking tools, which compute a single counter example only, our model checker allows the generation of all hazard-causing code sequences.