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

# Detecting Ladder Logic Bombs in IEC 61131-3 PLC Programs using ESBMC-PLC+: A Formal Verification Approach with Trigger Synthesis
Source: [https://arxiv.org/html/2607.08417](https://arxiv.org/html/2607.08417)
Pierre Dantas Department of Computer Science The University of Manchester Manchester, UK pierre\.dantas@manchester\.ac\.uk ORCID: 0000\-0001\-6390\-9340&Lucas Cordeiro11footnotemark:1 Department of Computer Science The University of Manchester Manchester, UK lucas\.cordeiro@manchester\.ac\.uk ORCID: 0000\-0002\-6235\-4272&Waldir Junior11footnotemark:1 Electrical Engineering Federal University of Amazonas \(UFAM\) Manaus, AM, Brazil waldirjr@ufam\.edu\.br ORCID: 0000\-0003\-3095\-0042The authors contributed equally to this research\. Corresponding author:pierre\.dantas@manchester\.ac\.uk\.

\(July 2026\)

###### Abstract

ALadder Logic Bombs \(LLB\)is malicious control logic inserted into aProgrammable Logic Controller \(PLC\)program that lies dormant until a*trigger*fires a*payload*which manipulates actuators, forges sensor readings, or denies operator control\. We make a structural observation about realLLBdatasets: the malicious logic hides*inside function\-block bodies*, which existingLadder Diagram \(LD\)verifiers drop from theirIntermediate Representation \(IR\), rendering the malicious and benign programs indistinguishable to the prover\. We presentESBMC\-LLB, a method that*uses ESBMC\-PLC\+*\(an existing IEC 61131\-3 verifier\) as its verification engine, adding a modeling layer that exposes the function\-block\-resident logic to the prover and recastsLLBdetection as formal verification: a*scan\-watchdog*exposes denial\-of\-control \(non\-termination\) payloads and*output wiring*exposes actuator\-forgery payloads as checkable safety violations\.k\-induction yields an*unbounded proof of bomb\-absence*across all scan cycles, and the bounded model checker returns a counterexample that*is the detonation trigger*– two guarantees that signature\-, anomaly\-, andControl Flow Graph \(CFG\)\-triage detectors do not provide\. On the publicIacobelliet al\.\[[12](https://arxiv.org/html/2607.08417#bib.bib12)\]dataset, ESBMC\-LLB detects all 30 bombs and recovers every trigger; because it reasons over program semantics rather than syntactic patterns, it also detects adaptive triggers \(computed, opaque\-arithmetic, multi\-scan\) that evade aCFG\-triage heuristic\. We further report the first evaluation of a semantic model checker on the state\-of\-the\-art’s real analog benchmark \(PLC\-Defuser’s SWaT corpus\): our analog modeling extension makes the full corpus parseable for the first time and, on the archived v1\.0\.0 release, detects149/150149/150bombs \(99%99\\%\) with zero false positives, recovering each trigger; on a later corpus version that adds*nonlinear*non\-termination bombs, detection drops to49%49\\%as theSatisfiability Modulo Theories \(SMT\)backend times out\. We conclude that semantic model checking andCFG\-triage are*complementary*– the former adds unbounded bomb\-absence proofs and adaptive\-trigger robustness and handles Boolean/integer and linear analog logic, the latter leads on nonlinear analog non\-termination – and we delineate exactly where each wins\.

*Keywords*Ladder Logic Bombs⋅\\cdotPLC⋅\\cdotIEC 61131\-3⋅\\cdotIndustrial Control Systems security⋅\\cdotESBMC⋅\\cdotBMC⋅\\cdotk\-induction⋅\\cdotSMT⋅\\cdottrigger synthesis⋅\\cdotformal verification⋅\\cdotLD⋅\\cdotPLCopen XML

## 1Introduction

Programmable Logic Controllers \(PLCs\)run the control logic of safety\-criticalIndustrial Control Systems \(ICS\): water treatment, power, chemical, and manufacturing plants\. An attacker who gains write access to aPLC– through the engineering workstation, a compromised project file, or the supply chain – can insert a*Ladder Logic Bombs \(LLB\)*: a fragment of control logic that remains dormant until a*trigger*fires, then executes a*payload*that sabotages the physical process\[[10](https://arxiv.org/html/2607.08417#bib.bib26)\]\. Unlike IT malware, anLLBis an ordinary ladder orStructured Text \(ST\)code; it passes commissioning tests and short simulations because its trigger is engineered to remain inactive during normal operation\.Govilet al\.\[[10](https://arxiv.org/html/2607.08417#bib.bib26)\]introduced the concept and a taxonomy ofLLBtriggers and payloads; subsequent work proposed detection architectures built on formal verification\[[12](https://arxiv.org/html/2607.08417#bib.bib12)\]and industrial deployment\[[3](https://arxiv.org/html/2607.08417#bib.bib14)\]\.

This paper makes that connection concrete and complete\. We build onESBMC\-PLC\+\[[6](https://arxiv.org/html/2607.08417#bib.bib20)\]– the unified IEC 61131\-3 verifier that accepts textualLadder Diagram \(LD\), graphicalLD, andST/Structured Control Language \(SCL\)through a singleEfficient SMT\-based Context\-Bounded Model Checker \(ESBMC\)backend withk\-induction – and observe that the machinery built for*safety*verification is, with no backend change, an*LLBdetector*\. We call the resulting methodESBMC\-LLB:

- •AnLLBpayload necessarily drives the program into a state that violates a safety or integrity property\. Detecting the bomb, therefore, reduces to checking that property\.
- •k\-induction discharges the property as an*unbounded*proof: a SAFE verdict certifies that*no*reachable scan\-cycle state detonates a bomb of the modeled class – a guarantee signature scanners cannot give\.
- •When a bomb is present,Bounded Model Checking \(BMC\)returns a counterexample trace\. That trace*is the trigger*: the exact input/cycle sequence that arms and fires the payload\. Detection thus yields automatictrigger synthesis\.

A stealthy and widely citedLLBclass is the counter/timer time\-bomb \(“detonate afterNNcycles”\)\[[10](https://arxiv.org/html/2607.08417#bib.bib26)\]: an integer\-state regime whereBinary Decision Diagrams \(BDD\)\-based unbounded provers are known to suffer state\-space explosion, whereas theSatisfiability Modulo Theories \(SMT\)bit\-vector engine ESBMC\-LLB builds on reasons about wide integer state symbolically\[[6](https://arxiv.org/html/2607.08417#bib.bib20)\]\. We use this property to recover counter/timer detonation triggers; we do*not*re\-measure the backend here, and we note up front \(§[6\.8](https://arxiv.org/html/2607.08417#S6.SS8)\) that this advantage does*not*extend to*nonlinear*integer state \(e\.g\. a non\-terminating loop updatingi := i\*i\), which remains hard for theSMTbackend and is where aControl Flow Graph \(CFG\)\-triage detector retains the edge\.

### 1\.1Contributions

1. 1\.A modeling layer that exposesFunctional Block \(FB\)\-resident bombs to ESBMC\-PLC\+\(§[6\.2](https://arxiv.org/html/2607.08417#S6.SS2)\): We show thatLLBs in the reference dataset hide*inside*LDfunction\-block bodies, which existingLDverifiers drop from theIntermediate Representation \(IR\); our modeling layer translates each function\-block body and feeds it to ESBMC\-PLC\+ \(whose verification engine is used unchanged\), making the bomb logic reachable to the prover\.
2. 2\.Two detection mechanisms with trigger synthesis: a*scan\-watchdog*that turns trigger\-gated non\-termination \(denial\-of\-control\) bombs into reachable safety violations, and*output wiring*that turns value/actuator\-forgery bombs into safety\-property violations; in both, theBMCcounterexample recovers the detonation trigger, andk\-induction certifies bomb\-absence unboundedly\.
3. 3\.Adaptive\-adversary robustness\(§[6\.6](https://arxiv.org/html/2607.08417#S6.SS6)\): because it evaluates program semantics rather than syntactic patterns, ESBMC\-LLB detects triggers \(computed, opaque\-arithmetic, multi\-scan\) engineered to evadeCFG\-based trigger triage – a class such detectors structurally miss\.
4. 4\.An honest evaluation, including a real head\-to\-head and a negative result\(§[6](https://arxiv.org/html/2607.08417#S6)\):30/3030/30detection on the publicIacobelliet al\.\[[12](https://arxiv.org/html/2607.08417#bib.bib12)\]dataset,100%100\\text\{\\,\}\\mathrm\{\\char 37\\relax\}recall with zero false positives on a 310\-program Boolean/integer corpus \(median70ms70\\text\{\\,\}\\mathrm\{ms\}\), and no regression \(13/1313/13\)\. We further present the first run of a semantic model checker on PLC\-Defuser’s real SWaT benchmark: our analog modeling extension makes the corpus parseable and, on the archived v1\.0\.0 release, detects149/150149/150bombs \(99%99\\text\{\\,\}\\mathrm\{\\char 37\\relax\}\) with zero false positives, while on a later corpus version that adds*nonlinear*non\-termination bombs detection drops to49%49\\text\{\\,\}\\mathrm\{\\char 37\\relax\}as theSMTbackend times out\.
5. 5\.A characterization of the semantic\-vs\-CFGtrade\-off\(§[7](https://arxiv.org/html/2607.08417#S7)\): semantic model checking leads on adaptive triggers and unbounded guarantees over Boolean/integer logic;CFG\-triage leads on nonlinear analog non\-termination\. The two are*complementary*, not competing\.

## 2Background and Related Work

### 2\.1ThePLCScan Cycle and ESBMC\-PLC\+

APLCexecutes a cyclic*scan*: it samples inputs, evaluates the control program once, writes outputs, and repeats, with a watchdog timer aborting the cycle if evaluation exceeds a fixed budget\. ESBMC\-PLC\+\[[6](https://arxiv.org/html/2607.08417#bib.bib20)\]encodes this scan cycle as awhile\(true\)loop in which inputs are re\-sampled nondeterministically \(an*open\-world*sensor model\), outputs and timer/counter state are persistent variables, and YAML\-specified safety/integrity properties are injected as\_\_ESBMC\_assert\(\)statements\. The resulting model is discharged by theESBMC\[[9](https://arxiv.org/html/2607.08417#bib.bib17),[18](https://arxiv.org/html/2607.08417#bib.bib18)\]backend:k\-induction proves a property holds for*all*scan counts \(an unbounded guarantee\)\. In contrast, incrementalBMCunrolls the loop to find a violating trace \(Fig\.[1](https://arxiv.org/html/2607.08417#S2.F1)\)\. We use this encoding unchanged and add only a modeling layer in front of it \(§[6\.2](https://arxiv.org/html/2607.08417#S6.SS2)\)\.

Sample inputsEvaluate program onceWrite outputswatchdog:abort if eval\>\>budgetPLC scan cyclewhile\(true\) \{in = nondet\(\);/\* outputs, timer/ \*//\* counter persist \*/step\(\);\_\_ESBMC\_assert\(p\);\}ESBMC\-PLC\+ encodingopen\-world sensor model⋅\\cdotpersistent state⋅\\cdotYAML propsESBMCbackendSAFE: holds for*all*scan counts\(k\-induction\)VIOLATION\+\+trace\(incrementalBMC\)

Figure 1:ThePLCscan cycle and its ESBMC\-PLC\+ encoding\. APLCrepeatedly samples inputs, evaluates the program once, and writes outputs, with a watchdog aborting an over\-budget evaluation\. ESBMC\-PLC\+ encodes the cycle as awhile\(true\)loop: inputs are re\-sampled nondeterministically \(open\-world sensor model\), outputs and timer/counter state persist across iterations, and YAML safety/integrity properties become\_\_ESBMC\_assert\(\)statements\.k\-induction proves a property for all scan counts \(unbounded\), while incrementalBMCunrolls the loop to return a violating trace\. Our modeling layer \(§[6\.2](https://arxiv.org/html/2607.08417#S6.SS2)\) sits in front of this encoding, which is used unchanged
### 2\.2Ladder Logic Bombs

Govilet al\.\[[10](https://arxiv.org/html/2607.08417#bib.bib26)\]defines aLLBby its*trigger*\(the activation condition\) and its*payload*\(the malicious effect\), and demonstrates bombs that manipulate actuators, forge sensor/HMI values, and deny control\. We reproduce this taxonomy in §[5](https://arxiv.org/html/2607.08417#S5)\. The threat is not hypothetical: the Stuxnet worm sabotaged centrifuge controllers by injecting maliciousPLClogic that remained dormant under inspection and detonated only under a precise process state\[[13](https://arxiv.org/html/2607.08417#bib.bib1)\];LLBs generalize this stealth pattern to arbitrary trigger/payload pairs, and their dormancy is exactly what defeats commissioning tests and short simulations\.

### 2\.3Related Detection Work

Table[1](https://arxiv.org/html/2607.08417#S2.T1)groups prior work by approach and positions ESBMC\-LLB: on Boolean/integerLDit matches dedicated detectors while uniquely adding unbounded bomb\-absence proofs and adaptive\-trigger robustness, whereas on nonlinear analog control PLC\-Defuser leads – so the two are complementary\.

Table 1:Positioning ESBMC\-LLB amongPLCmalicious\-/unsafe\-logic detectors\. “Sound absence proof” = certifies no bomb \(of the modelled class\) for*all*scan cycles; “Trigger synth\.” = recovers the concrete detonation condition; “Int\. trig\. scale” = behavior on integer\-comparison/counter triggers; “Adapt\. robust” = detects triggers engineered to evade syntactic/CFG triage\.†\\daggerESBMC\-LLB handles linear/flat integer arithmetic \(SMT\-BV\); PLC\-Defuser’s CFG triage localizes triggers structurally, handling nonlinear arithmetic without SMT\.Formal verification / model checking ofPLCcodeis the directly comparable line\.Iacobelliet al\.\[[12](https://arxiv.org/html/2607.08417#bib.bib12)\]\(ICPS’24\) is the closest competitor: a formal\-verification architecture forLLBdetection, evaluated on a public dataset of 30 legitimate and 30 malicious PLCopenLDprograms in which the bombs areEQ/LT/LE/GE/GTcomparison\-block triggers with coil/assignment payloads\. We use*their*dataset for our head\-to\-head \(§[6\.4](https://arxiv.org/html/2607.08417#S6.SS4)\)\. The*Trusted Safety Verifier \(TSV\)*\[[17](https://arxiv.org/html/2607.08417#bib.bib2)\]performs bump\-in\-the\-wire model checking ofPLCbytecode against safety properties, but is bounded and not spec\-free\.*SymPLC*\[[11](https://arxiv.org/html/2607.08417#bib.bib3)\]applies symbolic execution to IEC 61131\-3 via the same MATIEC\[[21](https://arxiv.org/html/2607.08417#bib.bib22)\]→\\toC path we use, but with KLEE – giving coverage\-driven test generation, not unbounded proofs\.*PLCverif*\[[22](https://arxiv.org/html/2607.08417#bib.bib7)\]is based onBounded Model Checking for ANSI\-C Programs \(CBMC\)orBDD\-bound \(nuXmv\[[5](https://arxiv.org/html/2607.08417#bib.bib19)\]\) and Siemens\-specific\. None of these provides an unbounded proof of bomb\-*absence*, automatic trigger synthesis, or robustness on integer triggers – the three axes on which ESBMC\-LLB leads\.

General IEC 61131\-3 verification:A broad line formalizes IEC 61131\-3 semantics and verifiesPLCcode for functional correctness and safety rather than malicious logic: executableSTsemantics\[[24](https://arxiv.org/html/2607.08417#bib.bib10),[14](https://arxiv.org/html/2607.08417#bib.bib11),[15](https://arxiv.org/html/2607.08417#bib.bib16)\], formal verification with inductive code synthesis\[[25](https://arxiv.org/html/2607.08417#bib.bib6)\], cooperative verification\[[23](https://arxiv.org/html/2607.08417#bib.bib8)\], ladder\-logic fault\-impact analysis\[[7](https://arxiv.org/html/2607.08417#bib.bib9)\], monitor\-based verification coupling FRET and PLCverif\[[8](https://arxiv.org/html/2607.08417#bib.bib13)\], and verification\-as\-a\-service deployments on safety\-critical plants\[[16](https://arxiv.org/html/2607.08417#bib.bib15)\]\. These tools verify a*specification of intended behavior*; none recastLLBdetection as an unbounded bomb\-absence proof with trigger synthesis, which is the gap ESBMC\-LLB fills\.

Invariant mining/safety vetting:*VetPLC*\[[26](https://arxiv.org/html/2607.08417#bib.bib4)\]\(CCS’19\) mines temporal invariants to vetPLCcode, and*SAIN*\[[1](https://arxiv.org/html/2607.08417#bib.bib5)\]\(USENIX’24\) refines state\-aware invariants; both target a different problem \(discovering specifications/anomalies\) and are complementary rather than head\-to\-head competitors\.

Runtime attestation and process\-levelMachine Learning \(ML\)anomaly detection\(e\.g\. on the SWaT testbed\) operate at a different layer \(network/sensor traces, not control logic\) and detect attacks at execution time rather than certifying the program offline\. We position against them qualitatively but do not claim a head\-to\-head\.

## 3Threat Model

We consider an adversary who targets aPLC\-controlled industrial process by inserting a dormantLLBinto the control program – a fragment that passes commissioning tests and short simulations because its trigger is engineered to remain inactive under normal operation\. The defender’s response is an offline, verification\-in\-the\-loop check that runs before the program is deployed to the plant\. Figure[2](https://arxiv.org/html/2607.08417#S3.F2)illustrates the resulting architecture; the two items below scope the attacker’s capability, and the defender’s posture\.

- •Adversary:An attacker with the ability to modify thePLCprogram \(a malicious insider, a compromised engineering station, or a tampered project/supply chain artifact\), but who must keep the bomb dormant during normal operation to evade review and testing\.
- •Defender:A verification\-in\-the\-loop process that runs ESBMC\-LLB on the deployed program against a set of safety/integrity properties derived from the plant specification\.

We assume a single\-task scan\-cycle model with an open\-world \(nondeterministic\) sensor model; that the supplied properties capture the hazardous or integrity\-violating states of interest \(or, for availability attacks, that scan non\-termination is itself hazardous\); and a trusted toolchain \(theESBMCbackend and the function\-block translation\)\. The adversary may obfuscate the trigger arbitrarily, but cannot alter the verifier or the property set\.

Adversary\(insider / eng\. station /supply\-chain tamper\)PLC program*dormant LLB*: trigger→\\topayloadPLCscan cyclePhysicalprocessESBMC\-LLBFB\-body translation\+\+scan\-watchdog\+\+output wiring*over*ESBMC\-PLC\+\(kk\-induction\+\+BMC\)SAFEunboundedbomb\-absenceVIOLATION\+\+detonationtriggerinsertsactuatesenseoffline check

Figure 2:Threat model and theESBMC\-LLBverification\-in\-the\-loop defence\. An adversary inserts a dormant ladder\-logic bomb into thePLCprogram 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\)\.
## 4Approach:LLBDetection as Property Checking

Table[2](https://arxiv.org/html/2607.08417#S4.T2)maps theGovilet al\.\[[10](https://arxiv.org/html/2607.08417#bib.bib26)\]taxonomy onto ESBMC\-PLC\+ property kinds\. The key observation is that every payload class has a natural safety/integrity property whose violation is necessary and sufficient for the bomb to have fired\.

Table 2:Govilet al\.\[[10](https://arxiv.org/html/2607.08417#bib.bib26)\]LLBtaxonomy mapped to ESBMC\-PLC\+ propertiesThe two verification outcomes follow directly from the property\-checking reduction: on a benign program, the prover certifies absence; on a bombed program, it returns the concrete detonation condition\. Both are products of the same backend, with no change to the underlying engine\.

- •Unbounded absence proof:For a benign program,k\-induction proves the property holds for all scan counts: a certificate that no bomb of the modeled class is present\.
- •Trigger synthesis:For a bombed program, incrementalBMCreturns the shortest counterexample; the input valuations and scan index along that trace constitute the detonation trigger\.

### 4\.1Two Detection Mechanisms

A bomb is detectable only once its payload \(a\) is present in the verifier’sIRand \(b\) violates a checkable property\. PriorLDverifiers fail \(a\) becauseLLBpayloads hide inside function\-block bodies that are dropped from theIR; §[6\.2](https://arxiv.org/html/2607.08417#S6.SS2)closes this with function\-block\-body translation\. Given the translated body, two mechanisms cover the two dominant payload families \(Figure[3](https://arxiv.org/html/2607.08417#S4.F3)\)\.

1. 1\.Scan\-watchdog\(denial\-of\-control / non\-termination\): A non\-terminating trigger\-gated loop is the canonical time\-bomb payload\. We instrument each rung loop with a bounded iteration counter asserted within budget – faithful to a realPLCwatchdog timer – so that a non\-terminating payload becomes a reachable safety violation\. The counterexample recovers the trigger\.
2. 2\.Output wiring with safety properties\(actuator/sensor forgery\): A value\-forgery payload changes a function\-block output\. By wiringFBoutput pins to the program variables that consume them, a forged output propagates into the program and violates a supplied safety property \(e\.g\.mutual\_exclusionon interlocked actuators\), again with trigger synthesis\.

Both mechanisms are*sound modulo the modeled class*: a payload that neither fails to terminate nor violates a stated property is out of scope, a limitation we make explicit \(§[7](https://arxiv.org/html/2607.08417#S7)\)\. A spec\-free*differential*alternative – checking a suspect program against a trusted reference for per\-scan output equivalence – is a natural extension and is left to future work, where “trusted reference” denotes a certified baseline or the pre\-update program version\.

LLBpayload hidden in a function\-block body\(a\) present in theIR?priorLDverifiers: FB body dropped⇒\\Rightarrowundetectable×\\timesdrop FBFB\-body translation \(§[6\.2](https://arxiv.org/html/2607.08417#S6.SS2)\)⇒\\Rightarrowpayload inIR✓\\checkmarktranslate\(b\) violates a checkable property?scan\-watchdog\(non\-termination\): assert counter≤\\leqbudgetoutput wiring\(forgery\): forgedFBoutput→\\tomutual\_exclusionreachable safety violation⇒\\RightarrowBMCcounterexample*is the trigger*

Figure 3:When anLLBis detectable\. A payload must be \(a\) present in the verifier’sIR*and*\(b\) violate a checkable property\. PriorLDverifiers drop function\-block bodies, so the payload never reaches theIR\(left\); ESBMC\-LLB’s function\-block\-body translation \(§[6\.2](https://arxiv.org/html/2607.08417#S6.SS2)\) restores it\. Two mechanisms then satisfy \(b\): a*scan\-watchdog*turns a non\-terminating payload into a bounded\-counter assertion, and*output wiring*makes a forgedFBoutput violate a supplied safety property \(e\.g\.mutual\_exclusion\)\. Either way, the violation is reachable, and theBMCcounterexample recovers the trigger

## 5LLBBenchmark Corpus

To evaluate ESBMC\-LLB across the full range of claims – third\-party detection accuracy, resistance to adaptive adversaries, scalability across the trigger/payload taxonomy, and head\-to\-head comparison on a real analog benchmark – we use four corpora assembled in increasing order of independence and difficulty \(Table[3](https://arxiv.org/html/2607.08417#S5.T3)\)\. Together they cover Boolean and integerLD, analog process control, and both synthetic and externally authored programs, ensuring that no single result rests on data we designed ourselves\.

Table 3:Evaluation corpora\. RQ identifiers refer to the Research Questions defined in §[6\.1](https://arxiv.org/html/2607.08417#S6.SS1)1. 1\.Third\-party dataset \(C1\):The publicIacobelliet al\.\[[12](https://arxiv.org/html/2607.08417#bib.bib12)\]dataset – 30 legitimate and 30 malicious PLCopenLDprograms modelling a water\-treatment process, with the bombs implemented as malicious function\-block wrappers \(EQ\_0/LE\_0/LT\_0/GE\_0/GT\_0/SUB\_0\) – provides detection results on data we did not create \(RQ2\)\.
2. 2\.Adaptive\-adversary variants \(C2\):Five semantically equivalent variants of one dataset bomb whose trigger is hidden from syntactic triage \(RQ4\)\.
3. 3\.Taxonomy corpus \(C3\):A controlled, reproducible generator emits benign/malicious pairs across 6 trigger classes×\\times2 payload classes×\\times13 constants \(310 Boolean/integer programs\) at the scale of the state\-of\-the\-art evaluation \(RQ5\)\.
4. 4\.PLC\-Defuser’s real SWaT corpus \(C4\):PLC\-Defuser’s tool and datasets are public\[[20](https://arxiv.org/html/2607.08417#bib.bib27)\]; its headline SWaT corpus \(150 legitimate\+\+150 malicious*analog*programs\) is the state\-of\-the\-art’s own benchmark\. We evaluate two pinned versions – the archived v1\.0\.0 release \(linear\-trigger bombs\) and a later development snapshot that adds nonlinear\-arithmetic bombs – as the real analog comparison \(RQ6\)\. All programs, properties, and harnesses are in the artifact \(§[8](https://arxiv.org/html/2607.08417#S8.SSx1)\)\.

## 6Experimental Evaluation

We structure the evaluation around seven research questions that together cover the full chain of claims made in this paper\. RQ1 establishes the enabling prerequisite – that function\-block\-body translation actually exposesFB\-resident bombs to the verifier – without which no downstream detection result is meaningful\. RQ2–RQ3 then assess detection accuracy and payload generality on third\-party and constructed programs, respectively\. RQ4–RQ6 progressively stress the approach: against an adaptive adversary, at the taxonomy scale on Boolean/integer logic, and finally on PLC\-Defuser’s real analog SWaT benchmark in a direct head\-to\-head comparison\. RQ7 closes with a regression check and a capability\-level comparison to the field\.

### 6\.1Research Questions

RQ1Enabling:Does the function\-block\-body translation makeLLBs that hide insideLDfunction blocks reachable to the verifier?

RQ2Detection on third\-party data:On the publicIacobelliet al\.\[[12](https://arxiv.org/html/2607.08417#bib.bib12)\]dataset \(30 legitimate \+ 30 maliciousLDprograms\), what detection rate, false\-positive rate, runtime, and trigger recovery does our approach achieve?

RQ3Generality:Does the approach detect bomb classes beyond non\-termination – specifically value/actuator\-forgery payloads with no loop?

RQ4Adaptive adversary:Does our approach detect triggers engineered to evade a syntactic/CFG\-based trigger\-triage heuristic?

RQ5Scale:Does detection hold at the scale of the state\-of\-the\-art evaluation on Boolean/integer logic, across the trigger/payload taxonomy?

RQ6Real head\-to\-head:On PLC\-Defuser’s own public SWaT benchmark, can our approach run, and how does it compare?

RQ7Regression and capability:Are all inherited ESBMC\-PLC\+ results preserved, and how does our approach compare by capability to the field \(Table[1](https://arxiv.org/html/2607.08417#S2.T1)\)?

### 6\.2Implementation and Setup

Our method uses ESBMC\-PLC\+ as the verification engine*unchanged*; the contribution is a lightweight modeling layer \(∼\\sim240 lines, plus a small Structured\-Text\-to\-GOTO translator\) that prepares a program for ESBMC\-PLC\+ to detect anLLB\. Three elements close the gap by whichLLBs evaded priorLDtools:

1. 1\.Function\-block\-body translation:Each user\-definedfunctionBlockProgram Organization Unit \(POU\)body is parsed and emitted as native GOTO code \(assignments,IF,WHILE, comparisons, arithmetic\), executed once per scan with nondeterministic inputs;
2. 2\.A scan\-watchdog:Each rung loop carries a bounded iteration counter asserted within budget, so a \(trigger\-gated\) non\-terminating payload becomes a reachable safety violation, faithful to the watchdog timer of a realPLC; and
3. 3\.Output wiring:AnFBoutput pin consumed by a program variable is assigned to that variable\. Hence, a forgedFBoutput propagates into the program and becomes observable by safety properties\.

For the analog benchmark \(RQ6\), we additionally extend the frontend with REAL types, non\-Boolean coils/contacts \(numeric–Boolean coercion\), and aSTtranslator that over\-approximates unsupported constructs; we distinguish this*analog\-extended configuration*from the*sound Boolean/integer configuration*used for RQ2–RQ5, because the over\-approximation trades soundness for coverage \(§[7](https://arxiv.org/html/2607.08417#S7)\)\. All experiments useESBMCv8\.3\.0 with the Z3 backend on Apple Silicon \(aarch64, macOS\);\-\-k\-inductionproves benign programs SAFE and\-\-incremental\-bmcsearches for violations\.

### 6\.3RQ1: Enabling – makingFB\-resident bombs visible

TheIacobelliet al\.\[[12](https://arxiv.org/html/2607.08417#bib.bib12)\]bombs are implemented*inside*function\-block bodies \(e\.g\. anEQ\_0wrapper that mimics equality but addsif IN1=12 then while…\)\. Inspecting the GOTOIRof the unmodified ESBMC\-PLC\+ confirms the root cause: the malicious program declares theFBinstance, but its body – and therefore the bomb – is*absent*from theIR; the malicious and benignIRare essentially identical so that no property can distinguish them\. With function\-block\-body translation the bomb logic appears in theIR\(theif IN1=12guard and the non\-terminating loop\), and a proof\-of\-concept on the sixFBtypes of the dataset \(EQ\_0/LE\_0/LT\_0/GE\_0/GT\_0/SUB\_0\) detects all six and recovers each trigger \(12 for the comparison FBs, 25 forSUB\_0\), with the benignFBproved SAFE\. This is the prerequisite for all subsequent results\. Figure[4](https://arxiv.org/html/2607.08417#S6.F4)shows the mechanism end\-to\-end on theEQ\_0bomb\.

\(\*MaliciousEQ\_0functionblock:bombhiddenintheFBbody\*\)

FUNCTION\_BLOCKEQ\_0

VAR\_INPUTIN1,IN2:INT;END\_VAR

VAR\_OUTPUTOUT:BOOL;END\_VAR

OUT:=\(IN1=IN2\);\(\*benignequality\*\)

IFIN1=12THEN\(\*dormanttrigger\*\)

WHILETRUEDO;END\_WHILE;\(\*denial\-of\-control\*\)

END\_IF;

END\_FUNCTION\_BLOCK

OUT=\(IN1==IN2\);

if\(IN1==12\)

for\(w=0;;\+\+w\)

\_\_ESBMC\_assert\(w<WD\_BUDGET\);

Figure 4:Enabling mechanism on theEQ\_0bomb\. The unmodifiedLDfrontend drops the function\-block body, so the malicious and benign programs share an identicalIR\. ESBMC\-LLB translates the body and instruments the rung loop with a scan\-watchdog assertion; the non\-terminating payload becomes a reachable safety violation whoseBMCcounterexample \(IN1==12\)*is*the trigger\. At the same time,k\-induction certifies that the block is benign\.
### 6\.4RQ2: Detection on theIacobelliet al\.\[[12](https://arxiv.org/html/2607.08417#bib.bib12)\]dataset

We run ESBMC\-LLB natively \(no MATIEC – these are PLCopenLD\) on all 60 programs of\[[12](https://arxiv.org/html/2607.08417#bib.bib12)\]\. Table[4](https://arxiv.org/html/2607.08417#S6.T4)reports the confusion matrix\.All 30 malicious programs are detected\(recall100%100\\text\{\\,\}\\mathrm\{\\char 37\\relax\}, zero false negatives\) and29 of 30 benign programs are proved SAFE with zero false positives; the single non\-SAFE benign program is*inconclusive*\(UNKNOWN\), not a false alarm – it is genuinely safe but its integer state defeatsk\-induction’s inductive step\. Detection is sub\-second per program\. The counterexample recovers the detonation trigger in every detected case \(constants 5, 12, 25, 30, 46, 54 across families\)\. This matches the “very high accuracy and precision” reported by\[[12](https://arxiv.org/html/2607.08417#bib.bib12)\]on the same data, while also providing unbounded proofs of the absence of bombs and automatic trigger synthesis\. These figures are for the sound Boolean/integer configuration; the analog\-extended configuration of RQ6, when applied to this same set, introduces one false positive \(§[7](https://arxiv.org/html/2607.08417#S7)\), which is why we keep the two configurations distinct\.

Table 4:Detection on theIacobelliet al\.\[[12](https://arxiv.org/html/2607.08417#bib.bib12)\]dataset \(60 programs\)
### 6\.5RQ3: Generality beyond non\-termination

The Iacobelli payloads are all non\-termination \(caught by the scan\-watchdog\)\. To test generality, we construct a*value/actuator\-forgery*bomb with*no loop*: a function block drives two interlocked actuators and, under a trigger value, forges bothTRUE, breaking the interlock\. With output wiring, the forged outputs reach the program; the benign program is proved SAFE for themutual\_exclusionproperty, while the bombed variant is reportedVIOLATIONwith the trigger \(TRIG=77\) recovered – detection via a*safety property*, a mechanism orthogonal to the watchdog\. Our approach thus covers two distinctLLBclasses \(denial\-of\-control and actuator forgery\) via two complementary mechanisms, each involving trigger synthesis \(Fig\.[5](https://arxiv.org/html/2607.08417#S6.F5)\)\.

Function block \(no loop\) IF TRIG = 77 THEN OUT1 := TRUE; OUT2 := TRUE;\(\* forge both \*\)ELSEnormal interlocked logicoutput wiring:OUT1→\\toA1,OUT2→\\toA2– forged outputs reach the programsafety propertymutual\_exclusion:¬\(A1∧A2\)\\lnot\(\\texttt\{A1\}\\wedge\\texttt\{A2\}\)\(interlock\)benign:SAFE\(k\-induction\)bombed:VIOLATIONtriggerTRIG=77 \(BMC\)no forgeforge

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 triggerTRIG=77, it forges bothOUT1andOUT2toTRUE, breaking the interlock\. Output wiring propagates the forged outputs to the program variablesA1,A2, so themutual\_exclusionproperty¬\(A1∧A2\)\\lnot\(\\texttt\{A1\}\\wedge\\texttt\{A2\}\)becomes checkable: the benign program is provedSAFEbyk\-induction, while the bombed variant is reportedVIOLATIONwith the trigger recovered\. This covers the actuator\-forgeryLLBclass through a mechanism orthogonal to the watchdog
### 6\.6RQ4: Adaptive adversary

A detector that*triages candidate triggers by syntactic/structural pattern*before checking \(theCFGstep of PLC\-Defuser\[[20](https://arxiv.org/html/2607.08417#bib.bib27)\]and signature scanners\) can be evaded by hiding the trigger while preserving behavior\. We construct five semantically equivalent variants of theEQ\_0bomb \(Table[5](https://arxiv.org/html/2607.08417#S6.T5)\) and compare our approach against a transparent*CFG\-triage proxy*that flags the canonical signature – an input equality\-compared to a constant literal guarding a payload\. The proxy flags only the naive baseline \(1/5\);our approach detects all five\(5/5\), because it evaluates the actual semantics rather than a pattern\. For the opaque\-arithmetic variants it even finds*bitvector\-overflow*detonating inputs \(e\.g\.IN1=1,073,840,131 withIN12≡144​\(mod​232\)\\texttt\{IN1\}^\{2\}\\equiv 144\\ \(\\mathrm\{mod\}\\ 2^\{32\}\)\) that the attacker’s intended±12\\pm 12arithmetic did not anticipate\. The proxy is a conservative model of syntactic triage, not PLC\-Defuser itself; the defensible claim is the general one:*pattern\-based triage is evadable, full semantic checking is not\.*

Table 5:Adaptive\-adversary variants of theEQ\_0bomb
### 6\.7RQ5: Scale on Boolean/integer logic

We evaluate at the scale of the state\-of\-the\-art evaluation on a controlled, reproducible bomb\-injection corpus of Boolean/integer programs spanning6 trigger classes×\\times2 payload classes×\\times13 constants==155 malicious\+\+155 benign==310 programs\. In this*sound \(Boolean/integer\) configuration*, our approach achieves100%100\\text\{\\,\}\\mathrm\{\\char 37\\relax\}recall \(155/155\) and zero false positives, with median detection time70ms70\\text\{\\,\}\\mathrm\{ms\}\(max305ms305\\text\{\\,\}\\mathrm\{ms\}\), uniform across all trigger classes \(including the hidden ones of RQ4\) and both payload classes\. This is a controlled scalability/breadth result; the third\-party validation is RQ2, and the real\-benchmark head\-to\-head is RQ6\.

### 6\.8RQ6: The real analog benchmark \(PLC\-Defuser SWaT\)

PLC\-Defuser’s tool and datasets are publicly available\[[20](https://arxiv.org/html/2607.08417#bib.bib27)\]\. We evaluate on its headline SWaT corpus \(150 legitimate\+\+150 malicious programs modeling the Secure Water Treatment plant\) in*two versions*that form two difficulty tiers: the archived releasev1\.0\.0\[[19](https://arxiv.org/html/2607.08417#bib.bib28)\], whose bombs are linear\-trigger non\-termination payloads, and a laterdevelopment snapshot\(commit\-pinned in our artifact\) that adds*nonlinear*\-arithmetic non\-termination bombs \(e\.g\.i := i\*i\)\. This is, to our knowledge, the*first*evaluation of a semantic model checker on this benchmark, and we report both tiers to delineate exactly where the approach holds and where it breaks\.

Parsing \(the enabling result\):SWaT is*analog*process control: programs drive non\-Boolean \(INT/REAL\) coils, use REAL arithmetic, and call timer function blocks\. The unmodifiedLDfrontend – Boolean\-ladder oriented – rejects≈\\approx95%95\\text\{\\,\}\\mathrm\{\\char 37\\relax\}of either version at parse time\. Our analog modeling extension \(REAL types, non\-Boolean coils, a tolerantSTtranslator\) makesall 300 programs parse, in both versions, for the first time\.

Detection on v1\.0\.0 \(linear triggers\):In the analog\-extended configuration, we detect149/150malicious programs \(Table[6](https://arxiv.org/html/2607.08417#S6.T6)\), with0/150 false positives, each in under a second; incrementalBMCrecovers the detonation trigger exactly for the input\- and timer\-gated cases \(e\.g\.IN1=20\)\. The fully*sound*configuration detects75/150– it covers every input\-triggered bomb but conservatively drops the exception\-wrapped \(\_\_TRY/\_\_CATCH\) and some timer payloads it cannot faithfully translate, rather than over\-approximate them\. These bombs are linear\-trigger non\-termination payloads, so99%99\\text\{\\,\}\\mathrm\{\\char 37\\relax\}detection demonstrates that the enabling pipeline – analog parsing, function\-block\-body translation, and the scan\-watchdog – works end\-to\-end on a*real*analog benchmark, not that it beats a hard problem\.

Detection on the development snapshot \(nonlinear triggers\):On the later corpus, detection drops to73/150\(Table[6](https://arxiv.org/html/2607.08417#S6.T6)\): we still detect the entire timer category \(50/50\), but the misses are non\-termination bombs whose loop bodies use*nonlinear*arithmetic \(i := i\*i\), which forces theSMTsolver to reason abouti2ki^\{2^\{k\}\}over the loop unrolling and times out\. We confirmed this is fundamental, not a tuning artifact: it persists across solvers \(Z3, Boolector\), unwind depths, and formula\-shrinking encodings\. PLC\-Defuser’sCFGtriage avoids this by structurally localizing the trigger, without solving the nonlinear formula\.

Table 6:ESBMC\-LLB on PLC\-Defuser’s SWaT benchmark, two corpus versions \(150 malicious, 150 legitimate each\)Honest reading:On linear\-trigger analog non\-termination ESBMC\-LLB detects99%99\\text\{\\,\}\\mathrm\{\\char 37\\relax\}with zero false positives and full trigger synthesis; on nonlinear\-arithmetic non\-termination it reaches only49%49\\text\{\\,\}\\mathrm\{\\char 37\\relax\}, clearly behind aCFG\-triage detector on its own harder corpus\. The two paradigms are*complementary*\(§[7](https://arxiv.org/html/2607.08417#S7)\): semantic model checking adds unbounded bomb\-absence proofs and adaptive\-trigger robustness and handles linear analog control\. At the same time,CFG\-triage leads to nonlinear analog non\-termination\. We do*not*claim parity on the nonlinear tier\.

### 6\.9RQ7: Regression and capability comparison

Re\-running the full ESBMC\-PLC\+ artifact benchmark suite under the extended frontend reproduces all inherited verdicts \(13/13\); theFB\-body translation, watchdog, and wiring introduce no regression on programs without user FBs \(untranslatableFBbodies fall back to a sound no\-op\)\. Table[1](https://arxiv.org/html/2607.08417#S2.T1)positions our approach against the field: on Boolean/integerLDit matches dedicated detectors and adds unbounded bomb\-absence proofs and adaptive\-trigger robustness; on nonlinear analog control, it is currently behind PLC\-Defuser \(RQ6\)\. SymPLC shares ourSTtranslation path but yields coverage rather than proofs;TSVand PLCverif are bounded; VetPLC addresses a complementary problem\.

## 7Discussion and Threats to Validity

Detection completeness:ESBMC\-LLB is sound for the modeled bomb classes \(non\-termination and property\-violating forgery\) but is*complete only modulo the supplied specification and these mechanisms*: a payload that always terminates and violates no stated safety property is out of scope\. This is the standard limitation of specification\-based detection; the watchdog mechanism narrows it by capturing availability attacks without a bespoke property\.

Soundness of the over\-approximation \(measured false positive\):The sound Boolean/integer configuration \(RQ2–RQ5\) produces zero false positives\. The analog\-extended configuration’s tolerant translator over\-approximates unsupported constructs \(function results, member access\) nondeterministically; this is the price of parsing analog programs, and it is*not*uniformly sound: it introducedone false positiveon the Iacobelli benign set \(29/30 SAFE, 1 SAFE\-program flagged\) that the sound configuration does not exhibit\. We therefore report the analog results as an exploratory frontier, with the strong soundness claims confined to the Boolean/integer configuration\.

Nonlinear arithmetic \(the limit on RQ6\):The archived v1\.0\.0 SWaT bombs are linear\-trigger non\-termination payloads, which we detect at99%99\\text\{\\,\}\\mathrm\{\\char 37\\relax\}\(RQ6\)\. The*development*version of the corpus adds non\-termination loops with nonlinear updates \(i := i\*i\); detecting these via the watchdog requires theSMTsolver to reason abouti2ki^\{2^\{k\}\}across the unrolling, which times out, dropping detection to49%49\\text\{\\,\}\\mathrm\{\\char 37\\relax\}\. We verified this is not a tuning artifact – it persists across solvers, unwind depths, and formula\-shrinking encodings – and reflects a genuine difference fromCFG\-triage, which localizes the trigger without solving the nonlinear formula\. Loop summarization/acceleration or aCFG\-guided hybrid is the natural remedy and is future work\.

Corpus realism:The scale corpus \(C3\) is synthetic and varies along the trigger/payload taxonomy from a shared host skeleton\. Third\-party validity rests on the Iacobelli set \(C1\) and on PLC\-Defuser’s real SWaT corpus \(RQ6\), which we did not author\.

Comparison to PLC\-Defuser:PLC\-Defuser’s tool and datasets are public, so RQ6 runs on its real SWaT benchmark in both corpus versions\. For the archived v1\.0\.0 release, we detect149/150149/150\(99%99\\text\{\\,\}\\mathrm\{\\char 37\\relax\}\) with zero false positives; for the later nonlinear\-bomb version, detection drops to49%49\\text\{\\,\}\\mathrm\{\\char 37\\relax\}, with PLC\-Defuser’sCFGtriage ahead\. The adaptive\-adversary comparison \(RQ4\) uses a transparentCFG\-triage*model*, not the tool itself; reproducing it with the released tool is left to future work\. We therefore claim*complementary*strengths, not superiority: parity on Boolean/integer logic and linear analog non\-termination, plus unbounded proofs and adaptive robustness, against PLC\-Defuser’s lead on*nonlinear*analog detection\.

Verification completeness:k\-induction is incomplete; one benign program \(C1\) is reportedUNKNOWNrather than SAFE\. Stronger invariant inference or a largerkkwould likely resolve it\.

Measurement validity:All runtimes are from a single Apple\-Silicon host \(ESBMCv8\.3\.0, Z3\); absolute timings will vary with hardware, solver, and solver version\. The*verdicts*\(SAFE / VIOLATION / UNKNOWN\) and the recovered triggers are deterministic and hardware\-independent, and the sub\-second medians leave a wide margin below any practical scan\-time budget, so we do not expect the qualitative conclusions to depend on the measurement platform\. A multi\-platform timing study is left to future work\.

## 8Conclusion

We presented a method that turns the ESBMC\-PLC\+ safety verifier into aLLBdetector\. The key observation is thatLLBs in real datasets hide insideLDfunction\-block bodies that prior verifiers drop from the intermediate representation; a∼\\sim240\-line function\-block\-body translation in the open\-sourceESBMCfrontend – with no backend change – makes them visible\. A scan\-watchdog and function\-block\-output wiring then expose, respectively, denial\-of\-control and actuator\-forgery payloads as checkable safety violations, and theBMCcounterexample recovers each detonation trigger\. At the same time,k\-induction certifies the absence of bombs unboundedly\. On the publicIacobelliet al\.\[[12](https://arxiv.org/html/2607.08417#bib.bib12)\]dataset, our approach detects all 30 malicious programs and recovers every trigger; on a 310\-program Boolean/integer taxonomy corpus, it sustains100%100\\text\{\\,\}\\mathrm\{\\char 37\\relax\}recall and zero false positives at a median70ms70\\text\{\\,\}\\mathrm\{ms\}; and, because it reasons over semantics rather than syntactic patterns, it detects adaptive triggers that a control\-flow\-graph triage misses\. On PLC\-Defuser’s real analog SWaT benchmark, we close the parsing gap that had prevented any semantic model checker from running on the corpus: on the archived v1\.0\.0 release, we detect149/150149/150bombs \(99%99\\text\{\\,\}\\mathrm\{\\char 37\\relax\}\) with zero false positives, while on a later corpus version that adds*nonlinear*non\-termination bombs detection drops to49%49\\text\{\\,\}\\mathrm\{\\char 37\\relax\}as theSMTbackend times out – the boundary where aCFG\-triage detector retains the edge\.

We therefore position semantic model checking andCFG\-triage as*complementary*\. For Boolean/integer ladder logic and linear analog non\-termination, our approach matches that of dedicated detectors\. It adds two guarantees their architecture lacks – unbounded bomb\-absence proofs and adaptive\-adversary robustness – whileCFG\-triage remains superior on*nonlinear*analog non\-termination\. Bridging the two \(loop summarization, or aCFG\-guided semantic check\) is a promising direction toward a detector that is both complete and sound across the full IEC 61131\-3 spectrum\.

### Artefact Availability

The implementation \(a branch of the open\-sourceESBMCLDfrontend adding function\-block\-body translation, the scan\-watchdog, and output wiring\), the three evaluation corpora \(the third\-party Iacobelli et al\. dataset, the adaptive\-adversary variants, and the taxonomy\-corpus generator\), all YAML property files, and the run harnesses accompany this paper\. A single binary reproduces both the sound Boolean/integer configuration and the analog\-extended configuration via the\-\-ld\-sound\-modeflag \(with\-\-ld\-scan\-watchdog/\-\-ld\-scan\-budgetcontrolling the scan\-watchdog\); the SWaT corpus is pinned to two fixed versions – the archived Zenodo v1\.0\.0 release and a commit\-pinned development snapshot – so both RQ6 tiers reproduce\.run\_all\.shruns all experiments andexpected/EXPECTED\.mdlists the reference results\.

For review, the artifact is provided through an anonymized repository linked from the submission; the permanent Zenodo archive and the underlying ESBMC\-PLC\+ artifact citation are withheld here to preserve anonymity and will be restored in the camera\-ready version\.

## Acknowledgements

The authors would like to express their gratitude to the Department of Computer Science at the University of Manchester \(UoM\) and the Systems and Software Security \(S3\) Research Group for their invaluable support, collaborative environment, and access to cutting\-edge resources, which were instrumental in the success of this research\. We conducted this work with partial funding from the Engineering and Physical Sciences Research Council \(EPSRC\) grants EP/T026995/1, EP/V000497/1, EP/X037290/1, and the Soteria project, awarded by the UK Research and Innovation under the Digital Security by Design \(DSbD\) Programme\.

## References

- \[1\]\(2024\-08\)SAIN: improving ICS attack detection sensitivity via state\-aware invariants\.InProceedings of the 33rd USENIX Security Symposium \(USENIX Security 2024\),Philadelphia, PA,pp\. 6597–6613\.External Links:[Link](https://dl.acm.org/doi/10.5555/3698900.3699269)Cited by:[§2\.3](https://arxiv.org/html/2607.08417#S2.SS3.p4.1),[Table 1](https://arxiv.org/html/2607.08417#S2.T1.5.3.15.12.1)\.
- \[2\]S\. Biallas, J\. Brauer, and S\. Kowalewski\(2012\-09\)Arcade\.plc: a verification platform for programmable logic controllers\.InProceedings of the 27th IEEE/ACM International Conference on Automated Software Engineering,ASE’12,Essen, Germany,pp\. 338–341\.External Links:[Document](https://dx.doi.org/10.1145/2351676.2351741)Cited by:[Table 1](https://arxiv.org/html/2607.08417#S2.T1.5.3.11.8.1)\.
- \[3\]R\. Bruttomesso, A\. Di Pinto, M\. Carullo, and A\. Carcano\(2024\)Method for automatic translation of ladder logic to a SMT\-based model checker in a network\.Note:US Patent 11,906,943\. Assignee: Nozomi Networks SAGLFiled: 2021\-08\-12\. Granted: 2024\-02\-20\.Cited by:[§1](https://arxiv.org/html/2607.08417#S1.p1.1)\.
- \[4\]J\. H\. Castellanos, M\. Ochoa, A\. A\. Cardenas, O\. Arden, and J\. Zhou\(2021\-10\)AttkFinder: discovering attack vectors in PLC programs using information flow analysis\.In24th International Symposium on Research in Attacks, Intrusions and Defenses,RAID ’21,Donostia/San Sebastián, Spain,pp\. 235–250\.External Links:[Document](https://dx.doi.org/10.1145/3471621.3471864)Cited by:[Table 1](https://arxiv.org/html/2607.08417#S2.T1.5.3.8.5.1)\.
- \[5\]R\. Cavada, A\. Cimatti, M\. Dorigatti, A\. Griggio, A\. Mariotti, A\. Micheli, S\. Mover, M\. Roveri, and S\. Tonetta\(2014\)The nuXmv symbolic model checker\.InComputer Aided Verification \(CAV 2014\),Lecture Notes in Computer Science, Vol\.8559,Vienna, Austria,pp\. 334–345\.External Links:[Document](https://dx.doi.org/10.1007/978-3-319-08867-9%5F22)Cited by:[§2\.3](https://arxiv.org/html/2607.08417#S2.SS3.p2.1)\.
- \[6\]P\. Dantas, L\. C\. Cordeiro, and W\. S\. Silva Júnior\(2026\)ESBMC\-PLC\+: unified IEC 61131\-3 formal verification framework with ST frontend and graphical function block support \(pull request \#5427\)\.Note:GitHub Pull Request \#5427,esbmc/esbmcSource code and benchmark suiteExternal Links:[Link](https://github.com/esbmc/esbmc/pull/5427)Cited by:[§1](https://arxiv.org/html/2607.08417#S1.p2.1),[§1](https://arxiv.org/html/2607.08417#S1.p4.1),[§2\.1](https://arxiv.org/html/2607.08417#S2.SS1.p1.1)\.
- \[7\]A\. Ebnenasir\(2023\)Formalizing ladder logic programs and timing charts for fault impact analysis and verification of fault tolerance\.Technical reportTechnical ReportCS\-TR\-23\-01,Michigan Technological University, Department of Computer Science\.External Links:[Link](https://www.mtu.edu/cs/research/papers/pdfs/formalizing-ladder-logic-ali-ebnenasir-tech-rpt-010623-rev.pdf)Cited by:[§2\.3](https://arxiv.org/html/2607.08417#S2.SS3.p3.1)\.
- \[8\]X\. Fink, A\. Mavridou, A\. Katis, and B\. F\. Adiego\(2024\)Verifying plc programs via monitors: extending the integration of fret and plcverif\.InNASA Formal Methods,pp\. 427–435\.External Links:ISBN 9783031606984,ISSN 1611\-3349,[Document](https://dx.doi.org/10.1007/978-3-031-60698-4%5F26)Cited by:[§2\.3](https://arxiv.org/html/2607.08417#S2.SS3.p3.1)\.
- \[9\]M\. R\. Gadelha, R\. S\. Menezes, and L\. C\. Cordeiro\(2020\-05\)ESBMC 6\.1: Automated Test Case Generation Using Bounded Model Checking\.International Journal on Software Tools for Technology Transfer23\(6\),pp\. 857–861\.External Links:[Document](https://dx.doi.org/10.1007/s10009-020-00571-2)Cited by:[§2\.1](https://arxiv.org/html/2607.08417#S2.SS1.p1.1)\.
- \[10\]N\. Govil, A\. Agrawal, and N\. O\. Tippenhauer\(2017\-09\)On ladder logic bombs in industrial control systems\.InComputer Security – ESORICS 2017 International Workshops, CyberICPS 2017 and SECPRE 2017,pp\. 110–126\.External Links:ISBN 9783319728179,ISSN 1611\-3349,[Document](https://dx.doi.org/10.1007/978-3-319-72817-9%5F8)Cited by:[§1](https://arxiv.org/html/2607.08417#S1.p1.1),[§1](https://arxiv.org/html/2607.08417#S1.p4.1),[§2\.2](https://arxiv.org/html/2607.08417#S2.SS2.p1.1),[Table 2](https://arxiv.org/html/2607.08417#S4.T2),[§4](https://arxiv.org/html/2607.08417#S4.p1.1)\.
- \[11\]S\. Guo, M\. Wu, and C\. Wang\(2017\-09\)Symbolic execution of programmable logic controller code\.InProceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering,ESEC/FSE’17,Paderborn, Germany,pp\. 326–336\.External Links:[Document](https://dx.doi.org/10.1145/3106237.3106245)Cited by:[§2\.3](https://arxiv.org/html/2607.08417#S2.SS3.p2.1),[Table 1](https://arxiv.org/html/2607.08417#S2.T1.5.3.3.2)\.
- \[12\]A\. Iacobelli, L\. Rinieri, A\. Melis, A\. A\. Sadi, M\. Prandini, and F\. Callegati\(2024\-05\)Detection of ladder logic bombs in PLC control programs: an architecture based on formal verification\.In2024 IEEE 7th International Conference on Industrial Cyber\-Physical Systems \(ICPS\),St\. Louis, MO, USA,pp\. 1–7\.External Links:[Document](https://dx.doi.org/10.1109/ICPS59941.2024.10639995)Cited by:[item 4](https://arxiv.org/html/2607.08417#S1.I2.i4.p1.7),[§1](https://arxiv.org/html/2607.08417#S1.p1.1),[§2\.3](https://arxiv.org/html/2607.08417#S2.SS3.p2.1),[Table 1](https://arxiv.org/html/2607.08417#S2.T1.5.3.7.4.1),[item 1](https://arxiv.org/html/2607.08417#S5.I1.i1.p1.1),[Table 3](https://arxiv.org/html/2607.08417#S5.T3.1.2.2.2),[itemRQ2](https://arxiv.org/html/2607.08417#S6.I1.ix2.p1.1),[§6\.3](https://arxiv.org/html/2607.08417#S6.SS3.p1.1),[§6\.4](https://arxiv.org/html/2607.08417#S6.SS4),[§6\.4](https://arxiv.org/html/2607.08417#S6.SS4.p1.1),[Table 4](https://arxiv.org/html/2607.08417#S6.T4),[§8](https://arxiv.org/html/2607.08417#S8.p1.6)\.
- \[13\]R\. Langner\(2011\-05\)Stuxnet: dissecting a cyberwarfare weapon\.IEEE Security & Privacy Magazine9\(3\),pp\. 49–51\.External Links:ISSN 1540\-7993,[Document](https://dx.doi.org/10.1109/msp.2011.67)Cited by:[§2\.2](https://arxiv.org/html/2607.08417#S2.SS2.p1.1)\.
- \[14\]J\. Lee and K\. Bae\(2024\-09\)Formal semantics and analysis of multitask PLC ST programs with preemption\.InFormal Methods – 26th International Symposium, FM 2024,pp\. 425–442\.External Links:ISBN 9783031711626,ISSN 1611\-3349,[Document](https://dx.doi.org/10.1007/978-3-031-71162-6%5F22)Cited by:[§2\.3](https://arxiv.org/html/2607.08417#S2.SS3.p3.1)\.
- \[15\]J\. Lee and K\. Bae\(2025\-10\)Formal analysis of networked PLC controllers interacting with physical environments\.InStatic Analysis – 32nd International Symposium, SAS 2025,pp\. 328–356\.External Links:ISBN 9783032071064,ISSN 1611\-3349,[Document](https://dx.doi.org/10.1007/978-3-032-07106-4%5F14)Cited by:[§2\.3](https://arxiv.org/html/2607.08417#S2.SS3.p3.1)\.
- \[16\]I\. D\. Lopez\-Miguel, B\. F\. Adiego, M\. Salinas, and C\. Betz\(2025\-06\)Formal verification of PLCs as a service: a CERN\-GSI safety\-critical case study\.InNASA Formal Methods – 17th International Symposium, NFM 2025,pp\. 227–235\.External Links:ISBN 9783031937064,ISSN 1611\-3349,[Document](https://dx.doi.org/10.1007/978-3-031-93706-4%5F13)Cited by:[§2\.3](https://arxiv.org/html/2607.08417#S2.SS3.p3.1)\.
- \[17\]S\. McLaughlin, S\. Zonouz, D\. Pohly, and P\. McDaniel\(2014\-02\)A trusted safety verifier for process controller code\.InProceedings 2014 Network and Distributed System Security Symposium \(NDSS’14\),NDSS 2014,San Diego, CA, USA\.External Links:[Document](https://dx.doi.org/10.14722/ndss.2014.23043)Cited by:[§2\.3](https://arxiv.org/html/2607.08417#S2.SS3.p2.1),[Table 1](https://arxiv.org/html/2607.08417#S2.T1.5.3.10.7.1)\.
- \[18\]R\. S\. Menezes, M\. Aldughaim, B\. Farias, X\. Li, E\. Manino, F\. Shmarov, K\. Song, F\. Brauße, M\. R\. Gadelha, N\. Tihanyi, K\. Korovin, and L\. C\. Cordeiro\(2024\)ESBMC v7\.4: Harnessing the Power of Intervals: \(Competition Contribution\)\.InTools and Algorithms for the Construction and Analysis of Systems \(TACAS 2024\),Lecture Notes in Computer Science, Vol\.14572,Luxembourg City, Luxembourg,pp\. 376–380\.External Links:[Document](https://dx.doi.org/10.1007/978-3-031-57256-2%5F24)Cited by:[§2\.1](https://arxiv.org/html/2607.08417#S2.SS1.p1.1)\.
- \[19\]L\. Rinieri, A\. Iacobelli, A\. Melis, M\. Prandini, and F\. Callegati\(2024\)PLC\_Defuser: tool and datasets \(swat, grfics, water\_tank\)\.Zenodo\.Note:Archived v1\.0\.0 release; the SWaT corpus used for the linear\-trigger tier of RQ6\.External Links:[Document](https://dx.doi.org/10.5281/zenodo.14014820)Cited by:[§6\.8](https://arxiv.org/html/2607.08417#S6.SS8.p1.1)\.
- \[20\]L\. Rinieri, A\. Iacobelli, A\. Melis, M\. Prandini, and F\. Callegati\(2026\-10\)PLC\-defuser: detecting hidden ladder logic bombs in plcs via control flow graph and model checking\.Computers & Security169,pp\. 104983\.External Links:ISSN 0167\-4048,[Document](https://dx.doi.org/10.1016/j.cose.2026.104983)Cited by:[Table 1](https://arxiv.org/html/2607.08417#S2.T1.4.2.2.2),[item 4](https://arxiv.org/html/2607.08417#S5.I1.i4.p1.1),[Table 3](https://arxiv.org/html/2607.08417#S5.T3.1.5.3.2),[§6\.6](https://arxiv.org/html/2607.08417#S6.SS6.p1.2),[§6\.8](https://arxiv.org/html/2607.08417#S6.SS8.p1.1)\.
- \[21\]E\. Tisserant, L\. Bessard, and M\. de Sousa\(2007\-07\)An open source iec 61131\-3 integrated development environment\.IEEE\.External Links:ISSN 1935\-4576,[Document](https://dx.doi.org/10.1109/indin.2007.4384753)Cited by:[§2\.3](https://arxiv.org/html/2607.08417#S2.SS3.p2.1)\.
- \[22\]J\. Tournier, B\. Fernández Adiego, and I\. D\. Lopez\-Miguel\(2021\-10\)PLCverif: status of a formal verification tool for programmable logic controller\.InProceedings of the 18th International Conference on Accelerator and Large Experimental Physics Control Systems \(ICALEPCS’21\),Shanghai, China,pp\. MOPV042\.External Links:[Document](https://dx.doi.org/10.18429/JACoW-ICALEPCS2021-MOPV042),ISBN 978\-3\-95450\-221\-9Cited by:[§2\.3](https://arxiv.org/html/2607.08417#S2.SS3.p2.1),[Table 1](https://arxiv.org/html/2607.08417#S2.T1.5.3.12.9.1)\.
- \[23\]C\. Ukegbu and H\. Mehrpouyan\(2023\-05\)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,San Antonio, TX, USA,pp\. 37–42\.External Links:[Document](https://dx.doi.org/10.1145/3576914.3587490)Cited by:[§2\.3](https://arxiv.org/html/2607.08417#S2.SS3.p3.1)\.
- \[24\]K\. Wang, J\. Wang, C\. M\. Poskitt, X\. Chen, J\. Sun, and P\. Cheng\(2023\-10\)K\-st: a formal executable semantics of the structured text language for plcs\.IEEE Transactions on Software Engineering49\(10\),pp\. 4796–4813\.External Links:ISSN 2326\-3881,[Document](https://dx.doi.org/10.1109/tse.2023.3315292)Cited by:[§2\.3](https://arxiv.org/html/2607.08417#S2.SS3.p3.1)\.
- \[25\]M\. Weis, P\. Marks, B\. Maschler, D\. White, P\. Kesseli, and M\. Weyrich\(2021\-07\)Towards establishing formal verification and inductive code synthesis in the PLC domain\.In2021 IEEE 19th International Conference on Industrial Informatics \(INDIN\),Palma de Mallorca, Spain,pp\. 1–8\.External Links:[Document](https://dx.doi.org/10.1109/INDIN45523.2021.9557423)Cited by:[§2\.3](https://arxiv.org/html/2607.08417#S2.SS3.p3.1)\.
- \[26\]M\. Zhang, C\. Chen, B\. Kao, Y\. Qamsane, Y\. Shao, Y\. Lin, E\. Shi, S\. Mohan, K\. Barton, J\. Moyne, and Z\. M\. Mao\(2019\-05\)Towards automated safety vetting of plc code in real\-world plants\.In2019 IEEE Symposium on Security and Privacy \(SP\),San Francisco, CA, USA,pp\. 522–538\.External Links:[Document](https://dx.doi.org/10.1109/sp.2019.00034)Cited by:[§2\.3](https://arxiv.org/html/2607.08417#S2.SS3.p4.1),[Table 1](https://arxiv.org/html/2607.08417#S2.T1.5.3.14.11.1)\.