pith. sign in

arxiv: 2606.18941 · v3 · pith:F3VKX2FXnew · submitted 2026-06-17 · 💻 cs.PL · cs.CL

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

Pierre Dantas , Lucas Cordeiro , Waldir Junior This is my paper

Pith reviewed 2026-06-26 18:56 UTC · model grok-4.3

classification 💻 cs.PL cs.CL
keywords PLC verificationLadder DiagramSMT model checkingGraphical programsIEC 61131-3Formal verificationGOTO IRPLCopen XML
0
0 comments X

The pith

A DFS-based resolver now turns graphical PLC Ladder Diagram connection graphs into full GOTO IR for SMT verification.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

ESBMC-PLC previously turned graphical PLCopen XML Ladder Diagram exports into empty intermediate representation, so verification always succeeded vacuously. The new resolver walks the directed graph of localId connections from leftPowerRail to each coil, builds Boolean conjunctions for each rung path, and uses three-tier I/O inference plus right-to-left coil ordering to match IEC 61131-3 scan-cycle rules. The resulting IR is handed to the unchanged ESBMC backend. On three graphical programs from CONTROLLINO and OpenPLC Editor the tool now produces complete IR containing nondeterministic inputs and rung logic, and all three programs are reported SAFE at bound k=2 in under 70 ms. The eleven existing textual benchmarks continue to pass unchanged.

Core claim

ESBMC-GraphPLC adds a DFS-based graphical LD resolver that traverses the connection graph from leftPowerRail to each coil, extracts rung paths as Boolean contact conjunctions, applies a three-tier I/O inference scheme, and orders coils by rightPowerRail connectionPointIn sequence. This produces full GOTO IR with nondeterministic inputs and rung logic for graphical programs, enabling verification of safety properties at small bound k=2. The graphical-to-IR conversion leaves the ESBMC backend unchanged, and the eleven textual LD benchmarks remain fully preserved.

What carries the argument

DFS-based graphical LD resolver that traverses the directed connection graph and applies three-tier I/O inference with coil ordering by rightPowerRail sequence.

If this is right

  • Graphical LD programs now generate complete GOTO IR containing rung logic instead of empty IR.
  • All three tested graphical programs verify SAFE at k=2 in under 70 ms.
  • Textual LD benchmarks continue to verify with no regression.
  • Beremiz files lacking LD content or using unsupported timers are reported as limitations.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same graph-walking technique could be applied to other graphical PLC formats whose exports expose similar connection graphs.
  • If coil ordering by connectionPointIn proves reliable across more editors, visual layout information itself becomes part of the formal semantics.
  • Extending the resolver to handle timers and other unsupported constructs would remove the remaining discovered limitations.

Load-bearing premise

The three-tier I/O inference scheme together with ordering coils by rightPowerRail connectionPointIn sequence correctly implements IEC 61131-3 scan-cycle semantics for the connection graphs exported by the tested editors.

What would settle it

A graphical program containing both SET and RESET coils whose rightPowerRail connectionPointIn order differs from the intended scan-cycle order; if the new tool reports SAFE while an equivalent textual version reports UNSAFE, the ordering rule is incorrect.

Figures

Figures reproduced from arXiv: 2606.18941 by Lucas Cordeiro, Pierre Dantas, Waldir Junior.

Figure 1
Figure 1. Figure 1: summarises the architecture of ESBMC-GraphPLC. The contribution of this paper is the Graphical LD Resolver & Rung Extractor module shown in the lower-left of the figure, which closes the gap described in Section 1 by traversing the connection graph, extracting equivalent rung expressions, and feeding them into the existing LD-to-GOTO-IR translation path unchanged. No part of the verification backend – GOTO… view at source ↗
Figure 2
Figure 2. Figure 2: rightPowerRail connectionPointIn sequence for water_control. Entry [0] references the SET coil and entry [1] references the RESET coil; this order, not coil position in the XML document, determines scan execution order. 5.5 DFS Rung Extraction (Line 5) For each leftPowerRail r and each coil q in ordered_coils, the DFS collects all simple paths from r to q. Each path becomes one RungNode: the contacts along… view at source ↗
read the original 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).

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 3 minor

Summary. The paper presents ESBMC-GraphPLC, an extension to ESBMC-PLC for verifying graphical PLCopen XML Ladder Diagram programs. It adds a DFS-based resolver that traverses the localId/refLocalId connection graph from leftPowerRail to coils, extracts rung paths as Boolean contact conjunctions, applies a three-tier I/O inference scheme, and orders coils by rightPowerRail connectionPointIn sequence to match IEC 61131-3 scan-cycle semantics (SET before RESET). The graphical-to-GOTO-IR conversion leaves the SMT-based model checker unchanged. Validation on three graphical LD programs from CONTROLLINO and OpenPLC Editor shows they now produce full IR containing nondeterministic inputs and rung logic (versus prior empty IR), all verify SAFE at k=2 in under 70 ms, and the eleven textual benchmarks exhibit no regression. Two Beremiz cases are reported as out-of-scope limitations.

Significance. If the results hold, the work is significant because it closes a practical gap in formal verification of industrial PLC programs: many editors export graphical rather than textual PLCopen XML, previously causing vacuous verification. The approach is pragmatic, reuses the existing ESBMC backend, preserves textual functionality, and ships a Zenodo artifact. It demonstrates that targeted graph traversal and inference rules suffice for the connection graphs produced by the tested editors, increasing the tool's applicability to real-world Ladder Diagram development without requiring changes to the core model checker.

major comments (1)
  1. [Abstract / validation section] Abstract and validation description: the claim that the three graphical programs now yield full IR and pass checks is supported by the reported outcomes, but the manuscript supplies no test-suite size, structural coverage metrics for the resolver, or comparison against an independent oracle for the extracted logic. This reduces the ability to assess whether the DFS traversal and three-tier I/O inference generalize even to other connection graphs from the same editors.
minor comments (3)
  1. [Resolver description] The three-tier I/O inference scheme is central to the resolver yet described only at a high level; a short pseudocode listing or explicit enumeration of the three tiers would improve clarity and reproducibility.
  2. [Validation] A small table or figure showing the generated GOTO IR fragment for one of the three graphical examples would help readers verify that nondeterministic inputs and rung logic are correctly emitted.
  3. [Limitations] The paper notes two Beremiz limitations but could briefly indicate whether the resolver's assumptions (e.g., presence of LD content or timer support) are documented in the artifact README.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the positive assessment and recommendation to accept. We address the single major comment below.

read point-by-point responses

  1. Referee: [Abstract / validation section] Abstract and validation description: the claim that the three graphical programs now yield full IR and pass checks is supported by the reported outcomes, but the manuscript supplies no test-suite size, structural coverage metrics for the resolver, or comparison against an independent oracle for the extracted logic. This reduces the ability to assess whether the DFS traversal and three-tier I/O inference generalize even to other connection graphs from the same editors.

    Authors: We agree that the validation uses only three graphical programs (plus eleven textual benchmarks) and provides neither structural coverage metrics nor an independent oracle. The resolver implements a deterministic left-to-right DFS over the PLCopen XML connection graph; therefore traditional coverage metrics do not apply, and correctness follows directly from the graph traversal definition together with the three-tier I/O inference rules and the IEC 61131-3 ordering of SET before RESET coils. To strengthen the presentation we will revise the validation section to (a) explicitly state the test-suite size, (b) describe the structural characteristics of the three programs (number of rungs, contacts per rung, coil types), and (c) note that the Zenodo artifact contains the complete extracted GOTO IR for each program, enabling manual or tool-based inspection by readers. We do not claim broad generalization beyond the tested editors. revision: partial

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper presents an engineering implementation of a DFS-based graphical LD resolver with three-tier I/O inference and rightPowerRail coil ordering to produce non-empty GOTO IR from PLCopen XML connection graphs. Central claims rest on direct empirical validation against three specific CONTROLLINO/OpenPLC Editor programs (full IR emitted, SAFE at k=2) plus unchanged textual benchmarks, with explicit out-of-scope notes for Beremiz cases. No equations, fitted parameters, predictions, or load-bearing self-citations reduce any result to its own inputs by construction; the resolver logic and scan-cycle semantics are presented as new code whose correctness is checked externally against editor outputs and IEC 61131-3 expectations.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The contribution rests on the domain assumption that the exported graphical connection graphs are well-formed directed graphs traversable by DFS and that the described coil ordering matches IEC scan-cycle rules; no free parameters or new entities are introduced.

axioms (2)
  • domain assumption Graphical PLCopen XML exports from CONTROLLINO, Beremiz, and OpenPLC Editor produce connection graphs whose left-to-right traversal yields the intended Boolean rung logic.
    Invoked when the resolver is described as extracting rung paths from leftPowerRail to coils.
  • domain assumption Ordering coils by rightPowerRail connectionPointIn sequence ensures SET coils are processed before RESET coils in the same scan cycle.
    Stated as matching IEC 61131-3 semantics.

pith-pipeline@v0.9.1-grok · 5796 in / 1348 out tokens · 27787 ms · 2026-06-26T18:56:33.335922+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

20 extracted references · 11 canonical work pages

  1. [1]

    Cordeiro, and W

    Pierre Dantas, Lucas C. Cordeiro, and W. S. Silva Júnior. GraphESBMC-PLC: Formal verification of graphical PLCopen XML ladder diagram programs using SMT-based model checking, 2026. URL https://doi.org/10. 5281/zenodo.20699856

    2026

  2. [2]

    Ock, Adsorb-agent open-source implementation,https://github.com/hoon-ock/ CatalystAIgent(2025), accessed 2026-04; archived athttps://doi.org/10.5281/zenodo

    Pierre Dantas, Lucas C. Cordeiro, and W. S. Silva Júnior. ESBMC-PLC: Formal verification of IEC 61131-3 ladder diagram programs using SMT-based model checking, 2026. URL https://doi.org/10.5281/zenodo. 20680071

    work page doi:10.5281/zenodo 2026

  3. [3]

    GraphESBMC-PLC: Graphical PLCopen XML support (pull request #5374)

    Pierre Dantas. GraphESBMC-PLC: Graphical PLCopen XML support (pull request #5374). https://github. com/esbmc/esbmc/pull/5374, 2026. GitHub pull request, merged 2026-06-15

    2026

  4. [4]

    Towards establishing formal verification and inductive code synthesis in the PLC domain

    Matthias Weiß, Philipp Marks, Benjamin Maschler, Dustin White, Pascal Kesseli, and Michael Weyrich. Towards establishing formal verification and inductive code synthesis in the PLC domain. InProceedings of the 19th IEEE International Conference on Industrial Informatics (INDIN 2021), 2021. https://doi.org/10.1109/ INDIN45523.2021.9557423. URLhttps://ieeex...

    arXiv 2021

  5. [5]

    PLCopen XML – technical specification, edition 2.01 ( tc6_0201)

    PLCopen. PLCopen XML – technical specification, edition 2.01 ( tc6_0201). https://plcopen.org/ technical-activities/xml-exchange, 2021. Accessed 2026-06-15

    2021

  6. [6]

    Springer Nature Switzerland, Luxembourg City, Luxembourg, 2024

    Rafael Sá Menezes, Mohannad Aldughaim, Farias, et al.ESBMC v7.4: Harnessing the Power of Intervals: (Competition Contribution), volume 14572 ofLecture Notes in Computer Science, page 376–380. Springer Nature Switzerland, Luxembourg City, Luxembourg, 2024. ISBN 9783031572562. https://doi.org/10.1007/ 978-3-031-57256-2_24

    2024

  7. [7]

    Gadelha, Rafael S

    Mikhail R. Gadelha, Rafael S. Menezes, and Lucas C. Cordeiro. ESBMC 6.1: Automated Test Case Generation Using Bounded Model Checking.International Journal on Software Tools for Technology Transfer, 23(6):857–861, May 2021. ISSN 1433-2787.https://doi.org/10.1007/s10009-020-00571-2

    work page doi:10.1007/s10009-020-00571-2 2021

  8. [8]

    Automated verification of temporal properties of ladder programs

    Cláudio Belo Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré, and Hiroaki Inoue. Automated verification of temporal properties of ladder programs. InF ormal Methods for Industrial Critical Systems (FMICS 2021), Lecture Notes in Computer Science. Springer, 2021. https://doi.org/10.1007/ 978-3-030-85248-1_2 . URL https://link.spring...

    work page doi:10.1007/978-3-030-85248-1_ 2021

  9. [9]

    Automated formal analysis of temporal properties of Ladder programs.International Journal on Software Tools for Technology Transfer, 2022

    Cláudio Belo Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré, and Hiroaki Inoue. Automated formal analysis of temporal properties of Ladder programs.International Journal on Software Tools for Technology Transfer, 2022. https://doi.org/10.1007/s10009-022-00680-0 . URL https: //link.springer.com/article/10.1007/s10009-022-00680-0

    work page doi:10.1007/s10009-022-00680-0 2022

  10. [10]

    Detection of ladder logic bombs in PLC control programs: an architecture based on formal verification

    Antonio Iacobelli, Lorenzo Rinieri, Andrea Melis, Amir Al Sadi, Marco Prandini, and Franco Callegati. Detection of ladder logic bombs in PLC control programs: an architecture based on formal verification. InProceedings of the IEEE 7th International Conference on Industrial Cyber-Physical Systems (ICPS 2024), 2024. https://doi.org/ 10.1109/ICPS59941.2024.1...

    work page doi:10.1109/icps59941.2024.10639995 2024

  11. [11]

    Method for automatic translation of ladder logic to a SMT-based model checker in a network

    Roberto Bruttomesso, Alessandro Di Pinto, Moreno Carullo, and Andrea Carcano. Method for automatic translation of ladder logic to a SMT-based model checker in a network. US Patent 11,906,943. Assignee: Nozomi Networks SAGL, 2024. URL https://patents.google.com/patent/US11906943B2/en. Filed: 2021-08-12. Granted: 2024-02-20. 17 ESBMC-GraphPLC

    2024

  12. [12]

    Lopez-Miguel, Jean-Charles Tournier, and Borja Fernández Adiego

    Ignacio D. Lopez-Miguel, Jean-Charles Tournier, and Borja Fernández Adiego. PLCverif: Status of a formal verification tool for programmable logic controller. InProc. ICALEPCS’21, number 18 in International Conference on Accelerator and Large Experimental Physics Control Systems, pages 248–252. JACoW Publishing, 2022. https://doi.org/10.18429/JACoW-ICALEPC...

    work page doi:10.18429/jacow-icalepcs2021-wepv004 2022

  13. [13]

    Lopez-Miguel, Borja Fernández Adiego, Matias Salinas, and Christine Betz

    Ignacio D. Lopez-Miguel, Borja Fernández Adiego, Matias Salinas, and Christine Betz. Formal verification of PLCs as a service: A CERN-GSI safety-critical case study. InNASA F ormal Methods (NFM 2025), Lecture Notes in Computer Science. Springer, 2025.https://doi.org/10.1007/978-3-031-93706-4_13 . Extended version: arXiv:2502.19150

    work page doi:10.1007/978-3-031-93706-4_13 2025

  14. [14]

    Bounded model checking of PLC ST programs using rewriting modulo SMT

    Jaeseo Lee, Sangki Kim, and Kyungmin Bae. Bounded model checking of PLC ST programs using rewriting modulo SMT. InProceedings of the 8th ACM SIGPLAN International Workshop on F ormal Techniques for Safety-Critical Systems (FTSCS 2022). ACM, 2022. https://doi.org/10.1145/3563822.3568016. URL https://dl.acm.org/doi/abs/10.1145/3563822.3568016

    work page doi:10.1145/3563822.3568016 2022

  15. [15]

    Formal semantics and analysis of multitask PLC ST programs with pre- emption

    Jaeseo Lee and Kyungmin Bae. Formal semantics and analysis of multitask PLC ST programs with pre- emption. InF ormal Methods (FM 2024), Lecture Notes in Computer Science. Springer, 2024. https: //doi.org/10.1007/978-3-031-71162-6_22 . URL https://link.springer.com/chapter/10.1007/ 978-3-031-71162-6_22

    work page doi:10.1007/978-3-031-71162-6_22 2024

  16. [16]

    Formal analysis of networked PLC controllers interacting with physical environments

    Jaeseo Lee and Kyungmin Bae. Formal analysis of networked PLC controllers interacting with physical environments. InStatic Analysis Symposium (SAS 2025). Springer, 2025. https:// doi.org/10.1007/978-3-032-07106-4_14 . URL https://link.springer.com/chapter/10.1007/ 978-3-032-07106-4_14

    work page doi:10.1007/978-3-032-07106-4_14 2025

  17. [17]

    Poskitt, Xiangxiang Chen, Jun Sun, and Peng Cheng

    Kun Wang, Jingyi Wang, Christopher M. Poskitt, Xiangxiang Chen, Jun Sun, and Peng Cheng. K-ST: A formal executable semantics of the structured text language for PLCs.IEEE Transactions on Software Engineering, 2023. https://doi.org/10.1109/TSE.2023.3315292. URLhttps://arxiv.org/abs/2202.04076

    work page doi:10.1109/tse.2023.3315292 2023

  18. [18]

    IEC-Checker: Static analysis of IEC 61131-3 programs

    Evgeny Suvorov and others. IEC-Checker: Static analysis of IEC 61131-3 programs. https://github.com/ jubnzv/iec-checker, 2021. Accessed 2026-06-15

    2021

  19. [19]

    OpenPLC examples: Water reserve control and staircase light control

    CONTROLLINO-PLC. OpenPLC examples: Water reserve control and staircase light control. GitHub repository (MIT License), 2024. URLhttps://github.com/CONTROLLINO-PLC/OpenPLC_examples. Programs created 2024-11-13, modified 2024-12-05. Hardware: CONTROLLINO MAXI Automation PLC

    2024

  20. [20]

    Formalizing ladder logic programs and timing charts for fault impact analysis and verification of fault tolerance

    Ali Ebnenasir. Formalizing ladder logic programs and timing charts for fault impact analysis and verification of fault tolerance. Technical Report CS-TR-23-01, Michigan Technological University, Department of Computer Science, 2023. URL https://www.mtu.edu/cs/research/papers/pdfs/ formalizing-ladder-logic-ali-ebnenasir-tech-rpt-010623-rev.pdf. 18

    2023