Programmable Logic Controllers (PLC) are widely used for industrial automation at CERN as they are also in industry. Reliable functionality of PLCs is crucial, but the released software is currently tested empirically. This project will develop a formal verification framework of PLC code, which will minimse downtime of critical installations and ensure safety.