Programmable logic controllers (PLC) are widely used in industries ranging from assembly lines, power plants, chemical processes to mining and rail automation. Such systems usually exhibit high safety requirements, and downtimes due to software errors entail intolerably high economic costs. Hence, their control programs are particularly suited for applying formal methods. The goal of this project is to investigate the application of existing and new model checking approaches to programmable logic controller code and to enhance these techniques to improve the applicability for industrial use. By adapting techniques known from compiler construction we found a new and efficient way of minimizing programs, which allows us to drastically reduce the size of the system under inspection. Using only this static precomputation we are already able to reduce the verification time by three orders of magnitude. To achieve the best possible performance we also aim to exploit modern multicore processors by parallel execution of highly diverse, state-of-the-art model checking approaches.