Sebastiaan Verhoek: SMT solver verification of ladder logic in a production environment (Tata Steel)

Posted on by Jan Friso Groote

Event Details

It is shown how to verify requirements on the PLC code in use at Tata Steel. A translator from PLC programs to the input language for SMT solvers has been written. Subsequently, requirements on some of the largest PLC programs available at Tata steel have been written down, and their validity on the software has been validated.