Ladder Diagram

SAFE-LD is ESBMC’s frontend for IEC 61131-3 Ladder Diagram (LD) programs — the graphical language used to program Programmable Logic Controllers (PLCs). It turns a Ladder Diagram, exported as PLCopen XML, into ESBMC’s internal representation so the engine’s bounded model checker and SMT backend can verify safety properties of the control logic — or prove their absence.

Properties are not written in the LD program itself; you supply them separately in a small YAML file. The frontend models the PLC’s cyclic scan (read inputs → evaluate rungs → drive outputs, repeated forever) and checks each property on every scan iteration.

The frontend is gated behind the ENABLE_LD_FRONTEND build option (off by default). See Usage for how to build and invoke it.