pith. sign in

arxiv: 2606.23870 · v2 · pith:LTGSTOSSnew · submitted 2026-06-22 · 💻 cs.PL · cs.CL· cs.SE

ESBMC-PLC+: A Unified IEC 61131-3 Formal Verification Framework as a PLCverif Successor

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

Pith reviewed 2026-06-26 05:36 UTC · model grok-4.3

classification 💻 cs.PL cs.CLcs.SE
keywords PLC verificationIEC 61131-3Formal verificationLadder DiagramStructured Textk-inductionESBMC
0
0 comments X

The pith

ESBMC-PLC+ unifies support for all IEC 61131-3 formats in one backend to deliver unbounded safety proofs for PLC programs.

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

The paper presents ESBMC-PLC+ as a successor to PLCverif that adds missing Ladder Diagram support and replaces the bounded CBMC backend with ESBMC. It routes Structured Text through the MATIEC compiler into ESBMC and models timer, counter, and edge-trigger blocks as persistent state variables in the GOTO IR. This combination lets the same tool handle textual, graphical, and mixed PLC inputs while using k-induction to prove properties for any number of cycles rather than only up to a fixed bound. A direct comparison on eight benchmark programs shows equivalent input coverage to PLCverif together with proofs on programs containing up to eight timers where the prior tool could not finish.

Core claim

ESBMC-PLC+ is the first open-source PLC verification framework to support all three major IEC 61131-3 input formats (Structured Text, Ladder Diagram, and PLCopen XML) via a single ESBMC backend, enabling k-induction-unbounded safety proofs. The framework achieves this through an ST frontend that compiles to C with nondeterministic inputs and YAML property injection, plus an extension of the DFS resolver that encodes TON/TOF/TP timers, CTU/CTD counters, and R_TRIG/F_TRIG triggers as scan-cycle-persistent state variables.

What carries the argument

Persistent scan-cycle state variables in the GOTO IR that encode the internal state of IEC 61131-3 timers, counters, and edge detectors.

If this is right

  • Ladder Diagram programs become verifiable for the first time in an open-source unbounded framework.
  • Programs with multiple integer timers can be proved safe without manual bounding of the search depth.
  • Verification time on timer-heavy benchmarks drops by two to three orders of magnitude compared with nuXmv BDD.
  • A single tool chain now covers the input formats that PLCverif already handled plus the dominant Ladder Diagram notation.

Where Pith is reading between the lines

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

  • Industrial users who currently rely on bounded checkers could switch to k-induction proofs without changing their property specifications.
  • The same state-variable modeling technique could be applied to other cyclic control languages that lack native unbounded verifiers.
  • Future extensions could add automated test-case generation from counter-examples produced by the k-induction engine.

Load-bearing premise

The translation of timer, counter, and edge-trigger blocks into persistent state variables in the GOTO IR preserves the exact cycle-by-cycle behavior of real PLC hardware.

What would settle it

A concrete PLC program containing at least one TON timer and one R_TRIG block for which ESBMC-PLC+ reports safety but a cycle-accurate hardware simulation or physical test rig shows a property violation within the first 100 scan cycles.

Figures

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

Figure 1
Figure 1. Figure 1: ESBMC-PLC+ ST/STL verification pipeline via MATIEC: the compiler translates IEC 61131-3 ST/STL to [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Left: PLC hardware architecture. Sensor signals are latched into the PII; the CPU executes the user program; [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: ESBMC internal architecture. Multiple source-language frontends compile to a unified GOTO program IR; [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: PLCverif architecture. Siemens SCL and FBD inputs are parsed into a GOTO-compatible IR; FRET [PITH_FULL_IMAGE:figures/full_fig_p006_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: ESBMC-PLC+ unified pipeline. The three frontends independently produce GOTO IR; the scan-cycle wrapper [PITH_FULL_IMAGE:figures/full_fig_p008_5.png] view at source ↗
read the original abstract

PLCverif is the most mature open-source platform for PLC formal verification, developed at CERN and in production use since 2019. Yet it has two fundamental limitations: no support for Ladder Diagram (LD) programs, the dominant PLC notation, and reliance on CBMC as its primary backend, which restricts verification to bounded proofs. The PLCverif authors themselves identified ESBMC as the appropriate backend improvement. Prior work established ESBMC-PLC (a textual LD frontend with k-induction) and ESBMC-GraphPLC (graphical PLCopen XML support); together, they cover LD with unbounded proofs but not Structured Text (ST), and graphical LD with timer/counter function blocks remains unverifiable. This paper presents ESBMC-PLC+, a unified framework that closes both gaps: (1) an ST/SCL frontend via the MATIEC IEC 61131-3 compiler, routing C-compiled ST to ESBMC with nondeterministic input modeling and YAML property injection; (2) function block state semantics for graphical LD, extending the DFS resolver to model TON/TOF/TP timers, CTU/CTD counters, and R_TRIG/F_TRIG edge triggers as persistent scan-cycle state variables in the GOTO IR. ESBMC-PLC+ is the first open-source PLC verification framework to support all three major IEC 61131-3 input formats via a single ESBMC backend, enabling k-induction-unbounded safety proofs. A feature comparison with PLCverif and experimental evaluation on 8 benchmark programs, including programs with up to 8 integer timers, shows that ESBMC-PLC+ matches PLCverif's input coverage while providing stronger guarantees. Against nuXmv's BDD backend, ESBMC-PLC+ is 400-2,000x faster on timer programs and completes proofs where nuXmv BDD times out at 120s.

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

2 major / 2 minor

Summary. The paper presents ESBMC-PLC+, a unified formal verification framework for IEC 61131-3 PLC programs. It integrates an ST/SCL frontend via the MATIEC compiler (with nondeterministic inputs and YAML properties) and extends the DFS resolver for graphical LD to model TON/TOF/TP timers, CTU/CTD counters, and R_TRIG/F_TRIG edges as persistent scan-cycle state variables in the GOTO IR. The central claim is that this is the first open-source tool supporting all three major input formats via a single ESBMC backend, enabling k-induction unbounded safety proofs; a feature comparison with PLCverif and results on 8 benchmarks (including programs with up to 8 timers) show matching coverage with stronger guarantees and 400-2000x speedups over nuXmv BDD on timer programs.

Significance. If the modeling holds, the work provides a practical advance by closing the LD gap in PLCverif while adding unbounded verification, which is valuable for industrial control systems. The unified backend, use of existing MATIEC compiler, and concrete performance numbers on timer-heavy benchmarks are strengths. The extension of prior ESBMC-PLC and ESBMC-GraphPLC work is a clear incremental contribution.

major comments (2)
  1. [function block state semantics for graphical LD / DFS resolver extension] The extension of the DFS resolver to encode timer/counter/edge function blocks as persistent GOTO IR state variables (described in the function block state semantics section) is load-bearing for the 'stronger guarantees' and 'correct semantics' claims, yet the manuscript provides no equivalence argument, reference semantics, or cross-validation against the IEC 61131-3 standard or a PLC runtime. Deviations in edge detection, timer resolution, or counter overflow would invalidate k-induction results for the LD case that PLCverif cannot handle.
  2. [experimental evaluation on 8 benchmark programs] Table or section reporting the 8 benchmark results: while programs with up to 8 timers are mentioned, there is no breakdown of which properties exercise the new timer/counter modeling or how the benchmarks were chosen to validate the persistent-state encoding, weakening the experimental support for the central claim.
minor comments (2)
  1. The abstract states that ESBMC-PLC+ 'matches PLCverif's input coverage' but the feature comparison table (if present) should explicitly list which formats each tool supports to make the 'first to support all three' claim easier to verify.
  2. Clarify the exact mechanism of 'YAML property injection' for ST programs, including an example, to aid reproducibility.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the positive assessment of the work's significance and the constructive major comments. We address each point below and indicate planned revisions to strengthen the manuscript.

read point-by-point responses

  1. Referee: The extension of the DFS resolver to encode timer/counter/edge function blocks as persistent GOTO IR state variables (described in the function block state semantics section) is load-bearing for the 'stronger guarantees' and 'correct semantics' claims, yet the manuscript provides no equivalence argument, reference semantics, or cross-validation against the IEC 61131-3 standard or a PLC runtime. Deviations in edge detection, timer resolution, or counter overflow would invalidate k-induction results for the LD case that PLCverif cannot handle.

    Authors: We agree that an explicit mapping to the standard would improve clarity. The function block modeling is derived directly from the IEC 61131-3 definitions: timers TON/TOF/TP use elapsed time and state variables updated per scan cycle; counters CTU/CTD handle increment/decrement with preset and current value, with overflow behavior as specified; edge detectors R_TRIG/F_TRIG compare current and previous input values across cycles. Persistent state in the GOTO IR models the PLC's scan-cycle persistence. We will add references to IEC 61131-3 clauses 2.5.2 (timers) and 2.5.3 (counters) along with a short equivalence description in the revised function block state semantics section. Formal cross-validation against a runtime is beyond the current scope but the encoding matches the standard operational semantics. revision: partial

  2. Referee: Table or section reporting the 8 benchmark results: while programs with up to 8 timers are mentioned, there is no breakdown of which properties exercise the new timer/counter modeling or how the benchmarks were chosen to validate the persistent-state encoding, weakening the experimental support for the central claim.

    Authors: The benchmarks include programs specifically designed or selected to exercise timer, counter, and edge function blocks (e.g., those with up to 8 timers) to validate the persistent-state encoding. We will expand the experimental evaluation section with a breakdown table listing for each of the 8 programs the input format, number and type of function blocks used, and the properties verified, highlighting which rely on the new LD modeling. This will also detail the selection criteria to demonstrate coverage of the extension. revision: yes

Circularity Check

0 steps flagged

No circularity: engineering tool paper with independent implementation claims

full rationale

The paper describes an engineering implementation that unifies frontends for ST/SCL and graphical LD (extending prior ESBMC-PLC work) and evaluates it on 8 benchmarks against PLCverif and nuXmv. No mathematical derivations, equations, fitted parameters, or predictions appear. Central claims rest on code-level modeling choices and runtime comparisons that are externally falsifiable via the released tool and benchmarks; self-citations to prior ESBMC-PLC papers are not load-bearing for any derivation because no result is justified solely by them. The modeling of timers/counters as persistent state variables is presented as an implementation decision, not derived from or equivalent to any input by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

The paper is a software tool development and implementation description rather than a mathematical derivation; it introduces no free parameters, axioms, or invented entities.

pith-pipeline@v0.9.1-grok · 5887 in / 1201 out tokens · 29230 ms · 2026-06-26T05:36:36.554659+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

21 extracted references · 11 canonical work pages

  1. [1]

    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. doi: 10.18429/JACoW-ICALEPCS2021-WEPV0...

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

  2. [2]

    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 Formal Methods (NFM 2025), Lecture Notes in Computer Science. Springer, 2025. doi: 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

  3. [3]

    Verifying PLC programs via monitors: Extending the integration of FRET and PLCverif

    Xaver Fink, Anastasia Mavridou, Andreas Katis, and Borja Fernandez Adiego. Verifying PLC programs via monitors: Extending the integration of FRET and PLCverif. InNASA Formal Methods (NFM 2024), volume 14627 ofLecture Notes in Computer Science. Springer, 2024. doi: 10.1007/978-3-031-60698-4_26. 20 ESBMC-PLC+: A Unified IEC 61131-3 Formal Verification Frame...

    work page doi:10.1007/978-3-031-60698-4_26 2024

  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. doi: 10.1109/INDIN45523.2021. 9557423

    work page doi:10.1109/indin45523.2021 2021

  5. [5]

    Cordeiro, and W

    Pierre Dantas, Lucas C. Cordeiro, and W. S. Silva Júnior. ESBMC-PLC: Formal verification of IEC 61131-3 ladder diagram programs, 2026. TACAS 2027 artefact. Reproducible viabash conformance/run_all.sh

    2026

  6. [6]

    Cordeiro, and W

    Pierre Dantas, Lucas C. Cordeiro, and W. S. Silva Júnior. ESBMC-GraphPLC: Formal verification of graphical PLCopen XML ladder diagram programs using SMT-based model checking, 2026

    2026

  7. [7]

    Cordeiro, and W

    Pierre Dantas, Lucas C. Cordeiro, and W. S. Silva Júnior. ESBMC-PLC+: Unified IEC 61131-3 formal verification framework with ST frontend and graphical function block support (pull request #5400). GitHub Pull Request #5400, esbmc/esbmc, 2026. URL https://github.com/esbmc/esbmc/pull/5400. Source code and benchmark suite

    2026

  8. [8]

    MATIEC: IEC 61131-3 compiler

    Mário de Sousa. MATIEC: IEC 61131-3 compiler. Open-source software, Beremiz project, 2014. URL https://github.com/beremiz/matiec. Accessed June 2026. Tested at commit7949c0b (Fix -Wvarargs and -Wdouble-promotion)

    2014

  9. [9]

    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

    2023

  10. [10]

    Gadelha, Norbert Tihanyi, Konstantin Korovin, and Lucas C

    Rafael Sá Menezes, Mohannad Aldughaim, Bruno Farias, Xianzhiyu Li, Edoardo Manino, Fedor Shmarov, Kunjian Song, Franz Brauße, Mikhail R. Gadelha, Norbert Tihanyi, Konstantin Korovin, and Lucas C. Cordeiro. ESBMC v7.4: Harnessing the Power of Intervals: (Competition Contribution). InTools and Algorithms for the Construction and Analysis of Systems (TACAS 2...

    work page doi:10.1007/978-3-031-57256-2_24 2024

  11. [11]

    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 2020. doi: 10.1007/s10009-020-00571-2

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

  12. [12]

    Springer Berlin Heidelberg,

    Leonardo de Moura and Nikolaj Bjørner.Z3: An Efficient SMT Solver, page 337–340. Springer Berlin Heidelberg,

  13. [13]

    In: Proc

    ISBN 9783540788003. doi: 10.1007/978-3-540-78800-3_24

    work page doi:10.1007/978-3-540-78800-3_24

  14. [14]

    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. doi: 10.1109/TSE.2023.3315292

    work page doi:10.1109/tse.2023.3315292 2023

  15. [15]

    Cooperative verification of PLC programs using CoVeriTeam: Towards a reliable and secure industrial control systems

    Chibuzo Ukegbu and Hoda Mehrpouyan. Cooperative verification of PLC programs using CoVeriTeam: Towards a reliable and secure industrial control systems. InProceedings of Cyber-Physical Systems and Internet of Things Week 2023 (CPS-IoT Week). ACM, 2023. doi: 10.1145/3576914.3587490

    work page doi:10.1145/3576914.3587490 2023

  16. [16]

    Cordeiro, and W

    Pierre Dantas, Lucas C. Cordeiro, and W. S. Silva Júnior. ESBMC-PLC+ vs nuXmv: IEC 61131-3 LD benchmark comparison — artefact, 2026. Benchmark suite, LD →SMV transpiler, and pre-computed results. Reproducible viabash run_all.sh

    2026

  17. [17]

    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. doi: 10.1109/ ICPS59941.2024.10639995

    arXiv 2024

  18. [18]

    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. Filed: 2021-08-12. Granted: 2024-02-20

    2024

  19. [19]

    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. InFormal Methods (FM 2024), Lecture Notes in Computer Science. Springer, 2024. doi: 10.1007/978-3-031-71162-6_22

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

  20. [20]

    Formal analysis of networked PLC controllers interacting with physical environments

    Jaeseo Lee and Kyungmin Bae. Formal analysis of networked PLC controllers interacting with physical environ- ments. InStatic Analysis Symposium (SAS 2025). Springer, 2025. doi: 10.1007/978-3-032-07106-4_14

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

  21. [21]

    Cordeiro, and W

    Pierre Dantas, Lucas C. Cordeiro, and W. S. Silva Júnior. ESBMC-PLC+: A unified IEC 61131-3 for- mal verification framework as a PLCverif successor — artefact, 2026. Permanently archived at Zen- odo. GitHub: https://github.com/pierredantas/esbmc-plcplus-artifact. Docker: docker pull ghcr.io/pierredantas/esbmc-plcplus-artifact:artifact. 21

    2026