ESBMC-PLC: Formal Verification of IEC 61131-3 Ladder Diagram Programs Using SMT-Based Model Checking

arXiv:2606.15461v2 Announce Type: replace-cross Abstract: Ladder diagram (LD) is the relay-circuit language of IEC 61131-3 in which many PLC safety interlocks are written, and model checkers built on SMT solvers do not read it. A verdict reached through a translation is only as good as that translation. We present ESBMC-PLC, which verifies LD programs with the ESBMC model checker, and argue that its translation is faithful. It encodes the scan cycle as a single loop with nondeterministic inputs, resolves graphical PLCopen XML networks into ordered rungs, models timers in milliseconds, and rejects programs outside an explicit subset.