Pith. sign in

REVIEW 3 major objections 29 references

Detecting Ladder Logic Bombs in IEC 61131-3 PLC Programs using ESBMC-PLC+: A Formal Verification Approach with Trigger Synthesis

T0 review · 3 major / 0 minor · reviewed 2026-07-10 · grok-4.5

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

Pith's one-line read Formal model checking of PLC ladder programs can expose hidden logic bombs and recover their detonation triggers, with unbounded proofs that pattern scanners lack.

desk verdict Solid, honest PLC-security paper: FB-body modeling turns an existing verifier into a real LLB detector with trigger synthesis and unbounded absence proofs, and they report the nonlinear failure instead of hiding it. read the letter →

arxiv 2607.08417 v1 pith:OMDYGYDL submitted 2026-07-09 cs.CL cs.AR

Pierre Dantas , Lucas Cordeiro , Waldir Junior This is my paper · ORCID
classification cs.CLcs.AR
keywords LadderLogicBombsPLCIEC61131-3formalverificationboundedmodelcheckingk-inductiontriggersynthesisindustrialcontrolsystems
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

Ladder Logic Bombs are ordinary-looking PLC control code that stay dormant until a trigger fires a payload that forges sensors, moves actuators, or hangs the controller. The paper shows that real bombs hide inside function-block bodies that ordinary ladder verifiers simply drop from their intermediate form, so the malicious and benign programs look identical to a prover. ESBMC-LLB restores those bodies, then turns bomb detection into ordinary safety checking: a scan-watchdog makes non-terminating denial-of-control payloads into assertion failures, and output wiring makes actuator-forgery payloads violate mutual-exclusion or integrity properties. Bounded model checking returns the concrete input sequence that is the trigger; k-induction can certify that no bomb of the modeled class exists across all scan cycles. On a public 60-program dataset the method finds every bomb and recovers every trigger; it also catches adaptive triggers that hide from control-flow triage, and on a real analog plant corpus it reaches 99 percent detection for linear cases while openly failing on nonlinear loops that time out the SMT solver.

What carries the argument

ESBMC-LLB modeling layer: function-block-body translation that re-injects the dropped logic into the prover, plus a scan-watchdog assertion and function-block output wiring that convert the two dominant payload families into reachable safety violations whose counterexamples are the triggers.

What would settle it

A planted ladder bomb whose payload always terminates and never violates any of the supplied safety or integrity properties, yet still produces a harmful physical effect that an operator would care about, would show the method is incomplete for real plant risk.

Watch

Extended reading notes

Core claim

Real ladder-logic bombs hide inside function-block bodies that prior ladder verifiers drop from the IR; once those bodies are restored and two lightweight mechanisms (scan-watchdog for non-termination, output wiring for forgery) are added, bomb detection reduces to ordinary safety verification. Bounded model checking synthesizes the detonation trigger as a counterexample, and k-induction supplies an unbounded certificate of bomb absence for the modeled classes.

Load-bearing premise

The method only catches bombs whose payloads either fail to terminate or violate a safety property the defender actually wrote down; a bomb that always finishes and never breaks a stated property stays invisible.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 0 minor

Summary. The paper presents ESBMC-LLB, a modeling layer atop the existing ESBMC-PLC+ verifier that recasts Ladder Logic Bomb (LLB) detection as formal property checking. The central observation is that real LLBs hide inside function-block bodies that prior LD frontends drop from the IR; a ~240-line FB-body translation, a scan-watchdog for non-termination payloads, and FB-output wiring for forgery payloads make those bombs checkable. k-induction yields unbounded bomb-absence proofs; incremental BMC recovers the detonation trigger. Evaluation covers the public Iacobelli et al. dataset (30/30 malicious, 0 FP among conclusive benign cases), five adaptive-trigger variants that evade a CFG-triage proxy (5/5), a 310-program Boolean/integer taxonomy corpus (100% recall, 0 FP, median 70 ms), and the first semantic model-checker run on PLC-Defuser’s SWaT corpus (149/150 on archived v1.0.0 linear bombs; 73/150 on a later nonlinear-arithmetic snapshot). The authors position semantic model checking and CFG triage as complementary rather than competing.

Significance. If the reported results hold, the work is a clear advance for offline PLC security verification. It supplies two guarantees that signature, anomaly, and CFG-triage detectors lack—unbounded bomb-absence certificates and automatic trigger synthesis—while remaining honest about where SMT-based checking loses (nonlinear analog non-termination). Strengths include: use of public third-party corpora (Iacobelli, PLC-Defuser SWaT) rather than only self-authored data; explicit reporting of the unfavorable nonlinear tier (49%) alongside the favorable linear tier (99%); a reproducible artifact with pinned corpus versions and a sound-mode flag; and a carefully scoped complementary framing versus CFG triage. These make the paper useful both as a detector and as a map of the semantic-vs-structural trade-off for the community.

major comments (3)
  1. §6.6 / Table 5: The adaptive-adversary claim is load-bearing for Contribution 3 and the “CFG-triage is structurally incomplete” positioning, yet the comparison is against a transparent CFG-triage proxy, not the released PLC-Defuser tool. The paper states this limitation, but the abstract and §1 still read as if the result is a head-to-head against CFG-triage detectors. Either (a) run the released PLC-Defuser tool on the five variants and report the outcome, or (b) rephrase abstract/intro claims to “evades a CFG-triage proxy modeling syntactic triage” so the contribution is not overstated relative to the evidence.
  2. §3, §4.1, §7: Detection completeness is explicitly modulo defender-supplied safety/integrity properties and the two modeled payload classes (non-termination, property-violating forgery). For a security detector this is a real operational boundary: an attacker who forges values that never violate the stated property set, or who uses a payload outside those two classes, is out of scope. The paper acknowledges this, but the threat-model and conclusion sections should state more sharply what the defender must supply (and what happens if the property set is incomplete) so that the “unbounded bomb-absence” guarantee is not read as absolute absence of all malicious logic.
  3. §6.8 / Table 6 and §7: The analog-extended configuration is reported to introduce one false positive on the Iacobelli benign set when applied outside RQ6, and the sound Boolean/integer configuration covers only 75/150 of the SWaT v1.0.0 bombs. The paper correctly separates the two configurations, but the abstract’s “149/150 … with zero false positives” line does not flag that this figure is from the over-approximating analog mode. A one-sentence qualification in the abstract (and a clearer callout in Table 6) would prevent readers from attributing full soundness to the 99% figure.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: detection claims are empirical measurements on external corpora, not quantities forced by the method's own definitions or fitted parameters.

full rationale

The paper's load-bearing claims are measured detection rates (Iacobelli 30/30, SWaT v1.0.0 149/150, adaptive variants 5/5, Boolean/integer taxonomy 155/155) and recovered triggers on third-party or controlled external programs. Recasting LLB detection as property checking (scan-watchdog for non-termination; output wiring for forgery) is a methodological reduction with an explicit completeness boundary (§4.1, §7), not a self-definitional loop: the paper still has to show that FB-body translation makes the payload reachable and that the BMC counterexample matches the detonation condition on real programs. Self-citation of ESBMC-PLC+ is use of the authors' prior verifier as an unchanged backend engine; the detection results do not reduce to claims proved only in that prior work, and the paper reports independent negative results (49% on nonlinear SWaT, one UNKNOWN under k-induction, one FP under analog over-approximation). There is no fitted parameter renamed as prediction, no uniqueness theorem imported from the authors, and no ansatz smuggled in via citation. The adaptive-adversary comparison is semantic checking versus a transparent CFG-triage proxy pattern, not a circular self-evaluation. Central claims are therefore self-contained against external benchmarks.

Assumptions & free parameters 2 free parameters · 5 assumptions · 3 invented entities

The central claims rest on a standard PLC scan-cycle encoding, an open-world nondeterministic sensor model, defender-supplied properties, a trusted translation/toolchain, and a watchdog budget that turns non-termination into a safety assertion. No physical constants are fitted; free parameters are engineering knobs (watchdog budget, solver/unwind settings). Invented constructs are modeling devices (scan-watchdog, output wiring, FB-body translation), not new physical entities. Completeness is explicitly modulo the modeled payload classes.

free parameters (2)
  • scan-watchdog budget (WD_BUDGET)
    Bounded iteration counter asserted per rung loop; chosen to mirror a real PLC watchdog and to make non-termination a reachable assertion. Detection of denial-of-control bombs depends on this budget being finite and enforced.
  • BMC unwind / solver timeout settings
    Incremental BMC depth and SMT timeouts determine whether nonlinear non-termination bombs are reported as timeouts versus violations; the 49% SWaT tier is sensitive to these engineering limits even though the paper argues the failure is fundamental.
assumptions (5)
  • domain assumption PLC execution is a single-task cyclic scan with persistent outputs/timers and nondeterministic open-world inputs each cycle.
    Stated in §2.1 and §3; the ESBMC-PLC+ while(true) encoding and all unbounded claims depend on this model.
  • domain assumption Supplied safety/integrity properties (or scan non-termination as hazardous) capture the defender’s hazardous states of interest.
    Threat model §3 and completeness discussion §7; detection reduces to property violation, so incomplete specs miss bombs.
  • domain assumption Function-block-body translation and the ESBMC backend are trusted and faithful for the sound Boolean/integer configuration.
    §3 trusted-toolchain assumption; if translation drops or mis-models payload logic, both detection and SAFE proofs fail.
  • standard math k-induction and bit-vector SMT reasoning are valid for the encoded scan loop and integer/Boolean state (standard formal-methods background).
    Used throughout for SAFE/VIOLATION verdicts; incompleteness of k-induction is acknowledged via one UNKNOWN benign case.
  • ad hoc to paper Analog-extended frontend may nondeterministically over-approximate unsupported ST constructs to gain parse coverage.
    §6.2 and §7; enables SWaT parsing but is not uniformly sound and produced one false positive on Iacobelli benign programs.
invented entities (3)
  • scan-watchdog instrumentation independent evidence
    purpose: Turn trigger-gated non-terminating payloads into reachable safety violations with recoverable triggers.
    Modeling device introduced in §4.1/§6.2; independent evidence is behavioral fidelity to real PLC watchdogs, not a new physical object.
  • function-block output wiring independent evidence
    purpose: Propagate forged FB outputs into program variables so actuator/sensor forgery violates stated safety properties.
    Modeling device for the forgery payload class (§4.1, RQ3); purpose is observability, not a new ontology of nature.
  • ESBMC-LLB modeling layer (~240 LOC FB-body translation) independent evidence
    purpose: Expose FB-resident bomb logic that prior LD verifiers drop from IR.
    Primary methodological invention (§6.2, RQ1); evidence is IR inspection and detection on public bombs, not external physical prediction.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Detecting Ladder Logic Bombs in IEC 61131-3 PLC Programs using ESBMC-PLC+: A Formal Verification Approach with Trigger Synthesis." pith.science (2026). https://pith.science/paper/OMDYGYDL

@misc{pith2026260708417,
  author       = {Pith},
  title        = {Pith review of: Detecting Ladder Logic Bombs in IEC 61131-3 PLC Programs using ESBMC-PLC+: A Formal Verification Approach with Trigger Synthesis},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/OMDYGYDL}},
  note         = {Machine review of arXiv:2607.08417}
}
read the original abstract

A Ladder Logic Bomb (LLB) is malicious control logic in a Programmable Logic Controller (PLC) program that lies dormant until a trigger activates a payload to manipulate actuators, forge sensor readings, or deny operator control. We observe that real malicious logic hides inside function-block bodies, which existing ladder-diagram verifiers drop from their intermediate representation (IR), making bombs invisible to provers. We present ESBMC-LLB, which uses ESBMC-PLC+ as its verification engine and adds a modeling layer that exposes function-block logic and recasts bomb detection as a formal verification problem: a scan-watchdog exposes non-termination payloads, and output wiring exposes actuator-forgery payloads as safety violations. k-induction gives an unbounded proof of bomb-absence across all scans, and the bounded model checker returns a counterexample that is the trigger - guarantees that signature, anomaly, and CFG-triage detectors lack. On the public Iacobelli 2024 dataset, ESBMC-LLB detects all 30 bombs and recovers every trigger; it also detects adaptive triggers (computed, opaque-arithmetic, multi-scan) that evade CFG-triage. We also report the first semantic model-checker evaluation on PLC-Defuser's SWaT corpus: our analog extension makes the full corpus parseable; on v1.0.0, it detects 149/150 bombs (99%) with zero false positives, recovering each trigger; on a later version with nonlinear non-termination bombs, detection drops to 49% as the SMT solver times out. We conclude that semantic model checking and CFG-triage are complementary - the former gives unbounded proofs, adaptive-trigger robustness, and handles Boolean/integer and linear analog logic; the latter leads to nonlinear analog non-termination, and we delineate where each wins.

Figures

Figures reproduced from arXiv: 2607.08417 by the authors.

Figure 1
Figure 1. The PLC scan cycle and its ESBMC-PLC+ encoding. A PLC repeatedly samples inputs, evaluates the [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Threat model and the ESBMC-LLB verification-in-the-loop defence. An adversary inserts a dormant ladder￾logic bomb into the PLC program driving the physical process; offline, ESBMC-LLB exposes the function-block￾resident payload, and either proves bomb-absence across all scan cycles (k-induction) or returns a counterexample that is the detonation trigger (BMC) [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. When an LLB is detectable. A payload must be (a) present in the verifier’s IR [PITH_FULL_IMAGE:figures/full_fig_p006_3.png] view at source ↗
Figures from the paper (2 more)
Figure 4
Figure 4. Figure 4: Enabling mechanism on the EQ 0 bomb. The unmodified LD frontend drops the function-block body, so the malicious and benign programs share an identical IR. ESBMC-LLB translates the body and instruments the rung loop with a scan-watchdog assertion; the non-terminating pa…
Figure 5
Figure 5. Figure 5: RQ3 generality: a no-loop actuator-forgery bomb, detected via a safety property rather than the scan￾watchdog. A function block drives two interlocked actuators; under the trigger TRIG=77, it forges both OUT1 and OUT2 to TRUE, breaking the interlock. Output wiring prop…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

29 extracted references · 29 canonical work pages

  1. [1]

    Berkay Celik, and Dongyan Xu

    Syed Ghazanfar Abbas, Muslum Ozgur Ozmen, Abdulellah Alsaheel, Arslan Khan, Z. Berkay Celik, and Dongyan Xu. SAIN: Improving ICS attack detection sensitivity via state-aware invariants. InProceedings of the 33rd USENIX Security Symposium (USENIX Security 2024), pages 6597–6613, Philadelphia, PA, August

    work page 2024

  2. [2]

    URLhttps://dl.acm.org/doi/10.5555/3698900.3699269

    USENIX Association. URLhttps://dl.acm.org/doi/10.5555/3698900.3699269

    work page doi:10.5555/3698900.3699269

  3. [3]

    Arcade.plc: a verification platform for programmable logic controllers

    Sebastian Biallas, J ¨org Brauer, and Stefan Kowalewski. Arcade.plc: a verification platform for programmable logic controllers. InProceedings of the 27th IEEE/ACM International Conference on Automated Software Engi- neering, ASE’12, page 338–341, Essen, Germany, September 2012. ACM. doi: 10.1145/2351676.2351741

    work page doi:10.1145/2351676.2351741 2012

  4. [4]

    Method for automatic trans- lation 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 trans- lation 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

  5. [5]

    Castellanos, Martin Ochoa, Alvaro A

    John H. Castellanos, Martin Ochoa, Alvaro A. Cardenas, Owen Arden, and Jianying Zhou. AttkFinder: Dis- covering attack vectors in PLC programs using information flow analysis. In24th International Symposium on Research in Attacks, Intrusions and Defenses, RAID ’21, pages 235–250, Donostia/San Sebasti ´an, Spain, October 2021. ACM. doi: 10.1145/3471621.3471864

    work page doi:10.1145/3471621.3471864 2021

  6. [6]

    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

  7. [7]

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

    Springer. doi: 10.1007/978-3-319-08867-9 22. 12 Detecting Ladder Logic Bombs in IEC 61131-3 PLC ProgramsPREPRINT

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

  8. [8]

    Cordeiro, and W

    Pierre Dantas, Lucas C. Cordeiro, and W. S. Silva J ´unior. ESBMC-PLC+: Unified IEC 61131-3 formal veri- fication framework with ST frontend and graphical function block support (pull request #5427). GitHub Pull Request #5427,esbmc/esbmc, 2026. URLhttps://github.com/esbmc/esbmc/pull/5427. Source code and benchmark suite

    work page 2026

Show all 29 references
  1. [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. URLhttps://www.mtu.edu/cs/research/papers/pd...

    2023

  2. [10]

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

    Xaver Fink, Anastasia Mavridou, Andreas Katis, and Borja Fern ´andez 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-...

    2024 doi

  3. [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

    2020 doi

  4. [12]

    Springer International Publishing, Oslo, Norway, September 2017

    Naman Govil, Anand Agrawal, and Nils Ole Tippenhauer.On Ladder Logic Bombs in Industrial Control Systems, pages 110–126. Springer International Publishing, Oslo, Norway, September 2017. ISBN 9783319728179. doi: 10.1007/978-3-319-72817-9 8

    2017 doi

  5. [13]

    Symbolic execution of programmable logic controller code

    Shengjian Guo, Meng Wu, and Chao Wang. Symbolic execution of programmable logic controller code. In Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, ESEC/FSE’17, pages 326–336, Paderborn, Germany, September 2017. ACM. doi: 10.1145/3106237.3106245

    2017 doi

  6. [14]

    Detec- tion 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. Detec- tion of ladder logic bombs in PLC control programs: An architecture based on formal verification. In2024 IEEE 7th International Conference on Industrial Cyber-Physical ...

    2024 doi

  7. [15]

    Stuxnet: Dissecting a cyberwarfare weapon.IEEE Security & Privacy Magazine, 9(3):49–51, May 2011

    Ralph Langner. Stuxnet: Dissecting a cyberwarfare weapon.IEEE Security & Privacy Magazine, 9(3):49–51, May 2011. ISSN 1540-7993. doi: 10.1109/msp.2011.67

    2011 doi

  8. [16]

    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

    2024 doi

  9. [17]

    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

    2025 doi

  10. [18]

    Lopez-Miguel, Borja Fern ´andez 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 ´andez 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.100...

    2025 doi

  11. [19]

    A trusted safety verifier for process controller code

    Stephen McLaughlin, Saman Zonouz, Devin Pohly, and Patrick McDaniel. A trusted safety verifier for process controller code. InProceedings 2014 Network and Distributed System Security Symposium (NDSS’14), NDSS 2014, San Diego, CA, USA, February 2014. Internet Society. doi: 10.1...

    2014 doi

  12. [20]

    Gadelha, Norbert Tihanyi, Konstantin Korovin, and Lucas C

    Rafael S ´a 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 Contribut...

    2024 doi

  13. [21]

    PLC Defuser: tool and datasets (swat, grfics, water tank), 2024

    Lorenzo Rinieri, Antonio Iacobelli, Andrea Melis, Marco Prandini, and Franco Callegati. PLC Defuser: tool and datasets (swat, grfics, water tank), 2024. Archived v1.0.0 release; the SWaT corpus used for the linear-trigger tier of RQ6

    2024

  14. [22]

    Plc-defuser: Detecting hidden ladder logic bombs in plcs via control flow graph and model checking.Computers & Security, 169: 104983, October 2026

    Lorenzo Rinieri, Antonio Iacobelli, Andrea Melis, Marco Prandini, and Franco Callegati. Plc-defuser: Detecting hidden ladder logic bombs in plcs via control flow graph and model checking.Computers & Security, 169: 104983, October 2026. ISSN 0167-4048. doi: 10.1016/j.cose.2026.104983

    2026 doi

  15. [23]

    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. 13 Detecting Ladder Logic Bombs in IEC 61131-3 PLC ProgramsPREPRINT

    2007

  16. [24]

    Lopez-Miguel

    Jean-Charles Tournier, Borja Fern´andez Adiego, and Ignacio D. Lopez-Miguel. PLCverif: Status of a formal ver- ification tool for programmable logic controller. InProceedings of the 18th International Conference on Acceler- ator and Large Experimental Physics Control Systems (...

    2021 doi

  17. [25]

    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, US...

    2023 doi

  18. [26]

    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.20...

    2023 doi

  19. [27]

    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, ...

    2021 doi

  20. [28]

    Morley Mao

    Mu Zhang, Chien-Ying Chen, Bin-Chou Kao, Yassine Qamsane, Yuru Shao, Yikai Lin, Elaine Shi, Sibin Mohan, Kira Barton, James Moyne, and Z. Morley Mao. Towards automated safety vetting of plc code in real-world plants. In2019 IEEE Symposium on Security and Privacy (SP), page 522...

  21. [29]

    doi: 10.1109/sp.2019.00034

    IEEE. doi: 10.1109/sp.2019.00034. 14

    2019 doi

Pith tools

Reviewed July 10, 2026 · model on record in the stance chip above.