arXiv:2606.18941v3 Announce Type: replace-cross 
Abstract: PLCopen XML defines two encoding formats for IEC 61131-3 Ladder Diagram programs: a textual encoding using <rung> elements, and a graphical encoding that represents rung logic as a directed graph of localId/refLocalId connections. ESBMC-PLC supported the textual format but parsed graphical exports from CONTROLLINO, Beremiz, and OpenPLC Editor into an empty GOTO intermediate representation, causing vacuous verification success. This paper presents ESBMC-GraphPLC, which closes this gap with a DFS-based graphical LD resolver. The resolver traverses the connection graph from leftPowerRail to each coil, extracts rung paths as Boolean contact conjunctions, and applies a three-tier I/O inference scheme. Ordering coils by rightPowerRail connectionPointIn sequence ensures SET coils process before RESET coils, matching IEC scan-cycle semantics. The graphical-to-IR conversion leaves the ESBMC backend unchanged. Validation on 3 graphical LD programs from CONTROLLINO/OpenPLC Editor shows all produce full GOTO IR with nondeterministic inputs and rung logic, versus the empty IR previously. All 3 verify SAFE at k=2 under 70ms. The 11 textual LD benchmarks are fully preserved, with no regression. Two Beremiz examples with no LD content or unsupported timer semantics are reported as discovered limitations. Artifact at Zenodo (DantasCordeiro2026graphical, doi:10.5281/zenodo.20699856).

يقدم المقال ESBMC-GraphPLC، أداة مصممة للتحقق الرسمي من برامج مخططات السلم XML PLCopen الرسومية باستخدام التحقق من النموذج المعتمد على SMT. يعالج هذا التطور القيود السابقة حيث تم معالجة الصادرات الرسومية من منصات مختلفة بشكل غير كاف، مما أدى إلى فشل التحقق.

El artículo presenta ESBMC-GraphPLC, una herramienta diseñada para la verificación formal de programas de diagramas de escalera XML PLCopen gráficos utilizando verificación de modelos basada en SMT. Este desarrollo aborda limitaciones anteriores donde las exportaciones gráficas de varias plataformas se procesaban de manera inadecuada, lo que conducía a fallos en la verificación.

L'article présente ESBMC-GraphPLC, un outil conçu pour la vérification formelle des programmes de diagrammes de relais en échelle XML PLCopen graphiques à l'aide de la vérification de modèle basée sur SMT. Ce développement répond aux limitations précédentes où les exports graphiques de diverses plateformes étaient traités de manière inadéquate, entraînant des échecs de vérification.

The paper introduces ESBMC-GraphPLC, a tool designed for the formal verification of graphical PLCopen XML Ladder Diagram programs using SMT-based model checking. This development addresses previous limitations where graphical exports from various platforms were inadequately processed, leading to verification failures.