Graph-ESBMC-PLC: Formal Verification of Graphical PLCopen XML Ladder Diagram Programs Using SMT-Based Model Checking

The paper introduces Graph-ESBMC-PLC, an enhancement to the ESBMC-PLC tool that enables formal verification of graphical PLCopen XML Ladder Diagram programs using a depth-first search (DFS) based resolver. This new approach successfully converts graphical rung logic into a full GOTO intermediate representation, addressing previous limitations where graphical exports resulted in vacuous verification. The tool demonstrated effective verification of three graphical LD programs, achieving a SAFE verification at k=2 in under 70ms, while maintaining full compatibility with existing textual LD benchmarks, making it a significant advancement for practitioners in automated PLC verification.