Pith. sign in

REVIEW 2 major objections 6 minor 36 references

Naive width-aware PLC verification raises 44% false alarms; a small hardware model restores soundness.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · grok-4.5

2026-07-10 05:31 UTC pith:3LLJHR62

load-bearing objection Clean empirical fix for a real soundness failure in width-aware PLC verification: 54 o0 false alarms on third-party code, with automatic bounds from %IW addresses. the 2 major comments →

arxiv 2607.08550 v1 pith:3LLJHR62 submitted 2026-07-09 cs.PL cs.ARcs.SYeess.SY

ESBMC-Arduino: Closing the Deployment Gap for Formal Verification of Open-Hardware PLCs

Pierre Dantas , Lucas Cordeiro , Waldir Junior This is my paper
classification cs.PL cs.ARcs.SYeess.SY
keywords deployment gaphardware-faithful verificationHAL descriptormachine word widthADC input modelIEC 61131-3open-hardware PLCbounded model checking
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

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

Open-hardware PLCs run IEC 61131-3 programs on cheap microcontrollers whose machine word is only 16 bits and whose sensors arrive through a finite-resolution ADC. Existing open-source verifiers prove safety over an abstract scan-cycle model that ignores both facts. The paper shows that simply checking 16-bit overflow without modelling the hardware inputs is unusable in practice: on 123 real third-party programs it produces a 44% false-alarm rate and finds zero genuine defects, because it invents sensor values no ADC can produce. The authors close the gap with a declarative HAL descriptor (word width, ADC/PWM resolution, I/O binding) and a sound lowering that interprets arithmetic at the target width while constraining every input to its hardware-realizable range. Instantiated for Arduino, the HAL annotator eliminates all 54 false alarms while preserving every robustness proof, and a controlled corpus isolates the rare, genuine width-dependent defects that can silently suppress a safety action such as a high-level tank alarm.

Core claim

The deployment gap between abstract IEC 61131-3 verification and the board artifact makes naive width-aware checking unsound in practice. On 123 real programs, 16-bit overflow checking without an input model yields 54 false alarms (44%) and zero true findings; an automatically derived HAL input model eliminates all of them while preserving the 32 robustness proofs, and detects genuine but rare width-dependent overflows only with physically realizable witnesses.

What carries the argument

The deployment model Mdev(P,H): a declarative four-field HAL descriptor H together with a faithful lowering that fixes arithmetic at the target word width and injects assume constraints that keep every input inside its hardware-realizable domain D(a).

Load-bearing premise

Soundness rests on the descriptor being faithful: the stated word width matches the board and every input domain covers the true hardware range; the evaluation treats every integer input as a uniform 10-bit ADC source and never executes the witnesses on physical boards.

What would settle it

Run the same 123 programs (or a larger analog-heavy corpus) on a physical AVR board while injecting the reported witnesses; if any of the 54 eliminated alarms actually overflows under real ADC readings, or if a program proved robust under the HAL model overflows on silicon, the soundness claim fails.

Watch this falsifier — get emailed when new claim-graph text bears on it.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

2 major / 6 minor

Summary. The paper identifies a deployment gap between abstract IEC 61131-3 verification (unbounded integers, free inputs) and open-hardware PLC execution (16-bit AVR words, finite-resolution ADC inputs). On 123 third-party programs, naive 16-bit overflow checking without an input model yields a 44% false-alarm rate (54/123) and zero genuine defects. The authors propose a declarative HAL descriptor (word width, ADC/PWM resolution, I/O map) and a sound lowering that interprets arithmetic at target width and constrains inputs to hardware-realizable ranges, instantiated as ESBMC-Arduino via a ~40-line frontend hook. Evaluation shows the HAL annotator eliminates all 54 false alarms while preserving 32 robustness proofs; a controlled taxonomy isolates rare width-dependent defects with realizable witnesses; CBMC and Frama-C reproduce both phantom and genuine cases, including on MATIEC-generated C.

Significance. The work transfers the target-model discipline of Frama-C/Astrée to the PLC domain with a decisive practical advantage: input bounds are recovered automatically from PLCopen %IW/%IX addresses rather than supplied as contracts. The empirical design is strong—same-binary HAL_ANNOTATE toggle, 16-vs-32 control isolating input-driven phantoms, cross-tool replication, and a self-contained artifact with pinned corpora and reproduce scripts. Honesty about rarity of genuine defects in public LD corpora and about k-induction incompleteness is a credit. If the result holds, it makes width-aware verification of open-hardware PLCs usable for assurance and ICS security testbeds, at low engineering cost.

major comments (2)
  1. [§5.4 Theorem 1; §10] §5.4 Theorem 1 and §10: Soundness is conditional on a faithful HAL H, and the evaluation is model-level only (no hardware-in-the-loop). The thesis is “what you verify must be what runs on the device,” yet the genuine-defect witnesses (e.g., adc=898 in §7.1) are never executed on a physical Uno/Due. A small HIL confirmation of at least one controlled-corpus flip, or a clearer argument why model-level fidelity to the official cores is sufficient for the claim, would strengthen the central deployment argument.
  2. [§8.2 RQ1; Abstract; §10] §8.2 RQ1 and §10: The prevalence claim that the gap is “rare” is scoped to integer/Boolean LD corpora dominated by Boolean/timer logic; analog-heavy process-control and ICS-testbed programs (where ADC-to-engineering-unit scaling is common) are outside the frontend. The abstract and introduction frame the problem as important for real automation and ICS security research. Either expand the controlled/real corpora with at least one analog-scaling industrial example, or more prominently qualify the prevalence claim in the abstract so the significance is not overstated relative to the evidence.
minor comments (6)
  1. [Abstract] Abstract names the instantiation “ArduinoTool”; title, body, and keywords use “ESBMC-Arduino.” Align the name throughout.
  2. [Table 5; §8.4; §10] Table 5 reports 32 safe / 91 unknown / 0 unsafe under HAL-annotated; the text sometimes says “91/123 programs are unknown” (§10) and elsewhere focuses on the 54→0 change. A single consistent accounting of the 37 already-unknown programs would help readers track RQ3 vs RQ4.
  3. [Listing 1; §7.1] Listing 1 and §7.1 use both “adc ≥ 819” and the counterexample adc=898; a one-line derivation of why 819 is the high-mark threshold (80% of 1023) would make the property fully self-contained.
  4. [Figure 2; §2.5] Figure 2 and §2.5 correctly locate the gap after MATIEC/cross-compilation; a brief note that the method verifies the pre-compilation model under target ABI assumptions (not the linked binary) would avoid any impression of binary-level verification.
  5. [Table 1; §3.1] Related-work Table 1 is clear; adding a row or footnote for PLCverif’s recent FRET/monitor extensions (§3.1) would keep the positioning current without changing the claim that none model target word width plus auto-derived input ranges.
  6. [§2.7; Artifact Availability] Minor typos: “A VR” spacing throughout (should be AVR); “hacked” in §2.7 should be “havocked”; “bun-dled” hyphenation in the artifact paragraph.

Circularity Check

0 steps flagged

No significant circularity: the 54 o0 false-alarm result is an empirical same-binary before/after on third-party corpora, not a quantity forced by definition or self-citation.

full rationale

The paper's central claim is an empirical measurement: naive 16-bit overflow checking on 123 third-party programs yields 54 false alarms that the HAL input-range model eliminates while preserving 32 robustness proofs. This is produced by toggling HAL_ANNOTATE on the same binary, with independent cross-tool replication on CBMC and Frama-C and on MATIEC-generated C. Theorem 1 is a standard state-set containment argument (Reach_dev ⊆ Reach_Mdev under a faithful descriptor H); it is not defined in terms of the evaluation outcome. Self-citations to the ESBMC-PLC line supply the LD frontend substrate but do not force the 54 o0 result by construction. HAL parameters are taken from official Arduino cores, not fitted to the corpus. The controlled corpus isolates width-dependent flips with realizable witnesses rather than renaming a known pattern. No fitted-input-called-prediction, uniqueness-imported-from-authors, or self-definitional step is present. Score 1 reflects only the ordinary self-citation of the authors' prior frontend work, which is not load-bearing for the soundness or evaluation claims.

Axiom & Free-Parameter Ledger

0 free parameters · 5 axioms · 2 invented entities

The central claim rests on standard PLC scan-cycle semantics, bit-precise two’s-complement arithmetic as modeled by ESBMC, and board parameters taken from official Arduino cores—not on fitted free parameters. The main modeling commitments are the faithful-HAL premise of Theorem 1, uniform 10-bit ADC treatment in evaluation, and sound over-approximation of non-linear blocks. Invented constructs are methodological (HAL descriptor, deployment model), not new physical entities.

axioms (5)
  • domain assumption PLC scan-cycle model: inputs resampled each scan, held constant during rung evaluation; safety is a per-scan assertion (open-world inputs, no continuous plant dynamics).
    Stated in §2.1 and §4.1.2; inherited from ESBMC-PLC encoding and used throughout evaluation.
  • domain assumption Target arithmetic is fixed-width two’s-complement at the board ABI int width (16-bit AVR, 32-bit ARM), with wrap outside [-2^{w-1}, 2^{w-1}).
    §2.6 and §5.1; parameters sourced from official Arduino cores / avr-gcc ABI.
  • ad hoc to paper For a faithful HAL H, Reach_dev ⊆ Reach_Mdev(P,H); non-linear FBs are replaced by nondeterministic outputs in declared ranges (Lemma 1).
    Theorem 1 and Appendix A; load-bearing for the claim that Mdev proofs imply device safety and that counterexamples are realizable.
  • domain assumption ESBMC’s bit-vector BMC/k-induction backend is sound for the encoded overflow VCs under the injected assumes.
    Method reuses backend unchanged (§5–6); confinement argument that the hook only adds assumes and sets width.
  • ad hoc to paper In the real-corpus evaluation, every integer input may be modeled as a 10-bit ADC reading in [0,1023] for AVR-class boards.
    §8.1 and §10; authors note mis-specified bounds would be unsound analogously to a wrong -machdep.
invented entities (2)
  • HAL descriptor H = ⟨w, b_adc, b_pwm, μ⟩ independent evidence
    purpose: Declarative board model that parameterizes word width, ADC/PWM resolution, and I/O role/domain binding for faithful lowering.
    Methodological construct derived from Arduino cores and PLCopen addresses; not a new physical object. Independent evidence is the match to published core parameters and the empirical 54→0 effect when applied.
  • Deployment model Mdev(P,H) vs abstract model Mabs independent evidence
    purpose: Formalize the deployment gap and gap diagnosis (safe under Mabs, unsafe under Mdev isolates width-induced defects).
    Definitional framework in §4–5; usefulness shown by controlled corpus flips and phantom elimination, not postulated as a new physical mechanism.

pith-pipeline@v1.1.0-grok45 · 26640 in / 3374 out tokens · 36051 ms · 2026-07-10T05:31:31.455640+00:00 · methodology

0 comments
read the original abstract

OpenPLC, Arduino OPTA, CONTROLLINO, and Industrial Shields M-Duino bring IEC 61131-3 to low-cost microcontrollers used in real automation and industrial control system (ICS) security research. Existing open-source verifiers for IEC 61131-3, including ESBMC-PLC, prove safety over an abstract scan-cycle model with idealized unbounded integers. The board artifact runs on a resource-constrained microcontroller unit (MCU) with 16-bit words (8-bit AVR Arduinos), and sensors are read via a finite-resolution analog-to-digital converter (ADC). We show this deployment gap makes naive width-aware verification unsound: across 123 real programs, checking 16-bit overflow without a hardware input model yields 44% false alarms (54/123) and finds no genuine defects, because it explores sensor values no ADC can produce. Since the gap lies where computation meets the physical process - a bounded sensor reading scaled by finite-width arithmetic into an actuation command - an overflow can silently suppress a safety action, such as a high-level alarm. An unbounded input model fabricates alarms that no environment can trigger. We present hardware-faithful verification for IEC 61131-3 on open hardware: a declarative hardware abstraction layer (HAL) descriptor (width, ADC/PWM resolution, I/O binding) and a sound lowering that interprets arithmetic at target width and constrains inputs to hardware-realizable ranges. We instantiate it for Arduino as ArduinoTool, deriving HAL parameters from official cores and realizing the input-range model in the ESBMC Ladder Diagram (LD) frontend. On the 123-program corpus, the HAL annotator eliminates all 54 false alarms while preserving robustness proofs, and a controlled corpus demonstrates the rare width-dependent defects it detects with realizable witnesses.

Figures

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

Figure 1
Figure 1. Figure 1: The HAL binds logical IEC 61131-3 variables to physical peripherals: Boolean [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Open-source PLC deployment: OpenPLC Editor [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Verification with ESBMC: BMC unrolls the scan loop [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: The cyber-physical loop of an open-hardware PLC. The deployment gap lies at the two interfaces where [PITH_FULL_IMAGE:figures/full_fig_p007_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Deployment gap as model agreement (diagonal) vs. disagreement (anti-diagonal) on [PITH_FULL_IMAGE:figures/full_fig_p008_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: ESBMC-Arduino pipeline. A PLCopen program is lowered to a GOTO IR; the faithful lowering (§5.3), [PITH_FULL_IMAGE:figures/full_fig_p009_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: The scan-cycle execution model. Each scan resamples the inputs, executes the program body once, and [PITH_FULL_IMAGE:figures/full_fig_p010_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Soundness as state-set containment (Theorem 1). Under a faithful descriptor [PITH_FULL_IMAGE:figures/full_fig_p011_8.png] view at source ↗

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

36 extracted references · 36 canonical work pages

  1. [1]

    Openplc: An iec 61131-3 compliant open source industrial controller for cyber security research.Computers & Security, 78:364–379, September 2018

    Thiago Alves and Thomas Morris. Openplc: An iec 61131-3 compliant open source industrial controller for cyber security research.Computers & Security, 78:364–379, September 2018. ISSN 0167-4048. doi: 10.1016/j.cose.2018.07.007

    work page doi:10.1016/j.cose.2018.07.007 2018

  2. [2]

    Openplc: An open source alternative to automation

    Thiago Rodrigues Alves, Mario Buratto, Flavio Mauricio de Souza, and Thelma Virginia Rodrigues. Openplc: An open source alternative to automation. InIEEE Global Humanitarian Technology Conference (GHTC 2014), page 585–589, San Jose, CA, USA, October 2014. IEEE. doi: 10.1109/ghtc.2014.6970342

    work page doi:10.1109/ghtc.2014.6970342 2014

  3. [3]

    Arduino OPTA: Micro PLC with industrial IoT

    Arduino. Arduino OPTA: Micro PLC with industrial IoT. https://www.arduino.cc/pro/ hardware-arduino-opta/, 2024. Accessed 2026-06-27

    work page 2024

  4. [4]

    Arduino PLC IDE: IEC 61131-3 programming for arduino pro hardware

    Arduino. Arduino PLC IDE: IEC 61131-3 programming for arduino pro hardware. https://www.arduino.cc/ pro/software-plc-ide/, 2024. Accessed 2026-06-27

    work page 2024

  5. [5]

    CONTROLLINO: Arduino-compatible industrial PLC

    CONTROLLINO. CONTROLLINO: Arduino-compatible industrial PLC. https://www.controllino.com/,

    work page

  6. [6]

    M-Duino arduino-based PLC family

    Industrial Shields. M-Duino arduino-based PLC family. https://www.industrialshields.com/, 2024. Accessed 2026-06-27

    work page 2024

  7. [7]

    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

    work page 2026

  8. [8]

    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

    work page 2026

  9. [9]

    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 #5427). GitHub Pull Request #5427, esbmc/esbmc, 2026. URL https://github.com/esbmc/esbmc/pull/5427. Source code and benchmark suite

    work page 2026

  10. [10]

    Lopez-Miguel

    Jean-Charles Tournier, Borja Fernández Adiego, and Ignacio D. Lopez-Miguel. PLCverif: Status of a formal verifi- cation tool for programmable logic controller. InProceedings of the 18th International Conference on Accelerator and Large Experimental Physics Control Systems (ICALEPCS’21), page MOPV042, Shanghai, China, October

    work page

  11. [11]

    Lopez-Miguel

    JACoW Publishing. ISBN 978-3-95450-221-9. doi: 10.18429/JACoW-ICALEPCS2021-MOPV042

    work page doi:10.18429/jacow-icalepcs2021-mopv042

  12. [12]

    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, pages 227–235

    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, pages 227–235. Springer Nature Switzerland, Williamsburg, V A, USA, June 2025. ISBN 9783031937064. doi: 10.1007/978-3-031-93706-4_13

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

  13. [13]

    Frama-c: A software analysis perspective.Formal Aspects of Computing, 27(3):573–609, May 2015

    Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski. Frama-c: A software analysis perspective.Formal Aspects of Computing, 27(3):573–609, May 2015. ISSN 1433-299X. doi: 10.1007/s00165-014-0326-7. 19 ESBMC-Arduino: Closing the Deployment Gap for Open-Hardware PLCsA PREPRINT

    work page doi:10.1007/s00165-014-0326-7 2015

  14. [14]

    The astreÉ analyzer

    Patrick Cousot, Radhia Cousot, Jêrome Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. The astreÉ analyzer. InProgramming Languages and Systems, page 21–30, Edinburgh, UK, 2005. Springer Berlin Heidelberg. ISBN 9783540319870. doi: 10.1007/978-3-540-31987-0_3

    work page doi:10.1007/978-3-540-31987-0_3 2005

  15. [15]

    ArduinoCore-avr: the official arduino avr core

    Arduino. ArduinoCore-avr: the official arduino avr core. https://github.com/arduino/ArduinoCore-avr,

    work page

  16. [16]

    Accessed 2026-06-28

    ADC 10-bit, analogWrite/PWM 8-bit; A VR-GCCint= 16-bit. Accessed 2026-06-28

    work page 2026

  17. [17]

    An open source iec 61131-3 integrated development environment, July 2007

    Edouard Tisserant, Laurent Bessard, and Mario de Sousa. An open source iec 61131-3 integrated development environment, July 2007. ISSN 1935-4576

    work page 2007

  18. [18]

    Smt-based bounded model checking for embedded ansi-c software.IEEE Transactions on Software Engineering, 38(4):957–974, July 2012

    Lucas Cordeiro, Bernd Fischer, and Joao Marques-Silva. Smt-based bounded model checking for embedded ansi-c software.IEEE Transactions on Software Engineering, 38(4):957–974, July 2012. ISSN 0098-5589. doi: 10.1109/tse.2011.59

    work page doi:10.1109/tse.2011.59 2012

  19. [19]

    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

  20. [20]

    Checking safety properties using induction and a sat-solver

    Mary Sheeran, Satnam Singh, and Gunnar Stålmarck. Checking safety properties using induction and a sat-solver. InFormal Methods in Computer-Aided Design, page 127–144, Berlin, 2000. Springer Berlin Heidelberg. ISBN 9783540409229. doi: 10.1007/3-540-40922-x_8

    work page doi:10.1007/3-540-40922-x_8 2000

  21. [21]

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

    Matthias Weis, Philipp Marks, Benjamin Maschler, Dustin White, Pascal Kesseli, and Michael Weyrich. Towards establishing formal verification and inductive code synthesis in the PLC domain. In2021 IEEE 19th International Conference on Industrial Informatics (INDIN), pages 1–8, Palma de Mallorca, Spain, July 2021. IEEE. doi: 10.1109/INDIN45523.2021.9557423

    work page doi:10.1109/indin45523.2021.9557423 2021

  22. [22]

    The nuXmv symbolic model checker

    Roberto Cavada, Alessandro Cimatti, Marco Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri, and Stefano Tonetta. The nuXmv symbolic model checker. InComputer Aided Verification (CAV 2014), volume 8559 ofLecture Notes in Computer Science, pages 334–345, Vienna, Austria,

    work page 2014

  23. [23]

    doi: 10.1007/978-3-319-08867-9_22

    Springer. doi: 10.1007/978-3-319-08867-9_22

    work page doi:10.1007/978-3-319-08867-9_22

  24. [24]

    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, 49 (10):4796–4813, October 2023. ISSN 2326-3881. doi: 10.1109/tse.2023.3315292

    work page doi:10.1109/tse.2023.3315292 2023

  25. [25]

    Springer Nature Switzerland, Milan, Italy, September 2024

    Jaeseo Lee and Kyungmin Bae.Formal Semantics and Analysis of Multitask PLC ST Programs with Preemption, pages 425–442. Springer Nature Switzerland, Milan, Italy, September 2024. ISBN 9783031711626. doi: 10.1007/978-3-031-71162-6_22

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

  26. [26]

    Springer Nature Switzerland, Singapore, Singapore, October 2025

    Jaeseo Lee and Kyungmin Bae.Formal Analysis of Networked PLC Controllers Interacting with Physical Environments, pages 328–356. Springer Nature Switzerland, Singapore, Singapore, October 2025. ISBN 9783032071064. doi: 10.1007/978-3-032-07106-4_14

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

  27. [27]

    Springer Nature Switzerland, Moffett Field, CA, USA, 2024

    Xaver Fink, Anastasia Mavridou, Andreas Katis, and Borja Fernández Adiego.Verifying PLC Programs via Monitors: Extending the Integration of FRET and PLCverif, page 427–435. Springer Nature Switzerland, Moffett Field, CA, USA, 2024. ISBN 9783031606984. doi: 10.1007/978-3-031-60698-4_26

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

  28. [28]

    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 ’23, pages 37–42, San Antonio, TX, USA, May 2023. ACM. doi: 10.1145/3576914. 3587490

    work page doi:10.1145/3576914 2023

  29. [29]

    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

    work page 2023

  30. [30]

    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

    work page 2024

  31. [31]

    Formal verification of a realistic compiler.Communications of the ACM, 52(7):107–115, July 2009

    Xavier Leroy. Formal verification of a realistic compiler.Communications of the ACM, 52(7):107–115, July 2009. ISSN 1557-7317. doi: 10.1145/1538788.1538814

    work page doi:10.1145/1538788.1538814 2009

  32. [32]

    Springer Berlin Heidelberg, Berlin, 2004

    Edmund Clarke, Daniel Kroening, and Flavio Lerda.A Tool for Checking ANSI-C Programs, page 168–176. Springer Berlin Heidelberg, Berlin, 2004. ISBN 9783540247302. doi: 10.1007/978-3-540-24730-2_15

    work page doi:10.1007/978-3-540-24730-2_15 2004

  33. [33]

    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. In2024 IEEE 7th 20 ESBMC-Arduino: Closing the Deployment Gap for Open-Hardware PLCsA PREPRINT International Conference on Industrial Cyber-Physical Syst...

    work page

  34. [34]

    Detec- tion of ladder logic bombs in PLC control programs: An architecture based on formal verification

    IEEE. doi: 10.1109/ICPS59941.2024.10639995

    work page doi:10.1109/icps59941.2024.10639995 2024

  35. [35]

    IEC 61131-3 clone detection dataset (plcopen xml / structured text)

    Kamil Rosiak et al. IEC 61131-3 clone detection dataset (plcopen xml / structured text). https://github.com/ KamilRosiak/IEC_61131_3_Clone_Detection, 2022. Accessed 2026-06-28

    work page 2022

  36. [36]

    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