ESBMC-PLC: Formal Verification of IEC 61131-3 Ladder Diagram Programs Using SMT-Based Model Checking

# ESBMC-PLC: Formal Verification of IEC 61131-3 Ladder Diagram Programs Using SMT-Based Model Checking
Source: [https://arxiv.org/html/2606.15461](https://arxiv.org/html/2606.15461)
Pierre Dantas Computer Science, The University of Manchester Manchester, UK pierre\.dantas@manchester\.ac\.uk &Lucas Cordeiro Computer Science, The University of Manchester Manchester, UK lucas\.cordeiro@manchester\.ac\.uk &Waldir Junior Electrical Engineering, Federal University of Amazonas \(UFAM\) Manaus, AM, Brazil waldirjr@ufam\.edu\.br

###### Abstract

Programmable Logic Controllers \(PLCs\)execute safety\-critical programs across industrial sectors where failures can cause catastrophic physical harm\. Despite their ubiquity, the dominantPLCprogramming notation –Ladder Diagram \(LD\), standardized inInternational Electrotechnical Commission \(IEC\)61131\-3 – has remained largely absent from the formal verification ecosystem: state\-of\-the\-artSatisfiability Modulo Theories \(SMT\)\-based model checkers cannot directly processLD’s graphical rung\-and\-coil notation\. This paper presentsESBMC\-PLC, the first open\-source formal verifier with native support forIEC61131\-3LDprograms in the standard PLCopen XML format, implemented as a new frontend for theEfficient SMT\-based Context\-Bounded Model Checker \(ESBMC\)model checker\. ESBMC\-PLC translatesLDrungs toESBMC’s GOTO intermediate representation, models thePLCscan cycle as awhile\(true\)loop with nondeterministic inputs, and checks user\-defined safety properties viaSMT\-based bounded model checking ork\-induction for unbounded proofs\. A five\-kind YAML property language \(mutual\_exclusion,invariant,absence,response,reachability\) allows automation engineers to specify safety requirements without expertise in temporal logic\. A systematic survey of 22 studies \(2020–2026\) identifies four research gaps inPLCLDformal verification; ESBMC\-PLC directly closes two of them\. The experimental evaluation on 13 benchmarks spanning 6 industrial domains and 3 program sources – including real programs from deployed CONTROLLINO PLCs and the MathWorks Simulink PLC Coder documentation – demonstrates correct classification of all 13 benchmarks across 61 verified properties – all 9 author\-constructed programs \(Categories A/B\) classified as expected by design, and all 4 independent vendor programs \(Category C, CONTROLLINO and MathWorks\) correctly classified without pre\-assigned labels – with 8 bugs found with actionable counterexamples, 7 unbounded safety proofs viak\-induction, and all runs completing in under60ms60\\text\{\\,\}\\mathrm\{ms\}on Apple Silicon \(aarch64\)\. A feature\-by\-feature comparison with PLCverif shows that ESBMC\-PLC is the only open\-source tool combining nativeLDinput,k\-induction unbounded proofs, andSMTbit\-vector semantics\.

*K*eywordsPLC, Ladder Diagram,LD, IEC 61131\-3,ESBMC,BMC,k\-induction,SMT\-Based Verification, Formal Methods, PLCopen XML, Industrial Control Systems, ESBMC\-PLC

## 1Introduction

Industrial automation systems depend onProgrammable Logic Controllers \(PLCs\)to execute timed, event\-driven control programs in real time\.PLCsgovern actuators, read sensor inputs, and maintain safety interlocks in nuclear power plants, water treatment facilities, chemical refineries, railway signalling systems, and automotive production lines\. A failure inPLCcontrol logic – whether caused by a design defect, a specification violation, or a maliciously injected code segment – can propagate into physical harm: toxic releases, equipment destruction, or loss of human life\. The Stuxnet incident demonstrated thatPLCprograms are a viable attack surface\[[23](https://arxiv.org/html/2606.15461#bib.bib4)\], and subsequent research has confirmed thatLadder Logic Bombs \(LLB\)attacks – covert modifications ofPLClogic that activate under specific trigger conditions – can evade conventional testing\[[12](https://arxiv.org/html/2606.15461#bib.bib16),[3](https://arxiv.org/html/2606.15461#bib.bib19)\]\.

The appropriate response to this threat profile is formal verification: mathematical techniques that prove the presence or absence of a property across*all*possible execution traces, rather than testing a finite sample\. Formal verification has matured substantially for general\-purpose software\. TheEfficient SMT\-based Context\-Bounded Model Checker \(ESBMC\)model checker can verify C, C\+\+, Python, Kotlin, Rust, Solidity, andCompute Unified Device Architecture \(CUDA\)programs, automatically checking arithmetic overflow, array out\-of\-bounds access, null\-pointer dereference, and user\-defined safety assertions\[[20](https://arxiv.org/html/2606.15461#bib.bib41),[10](https://arxiv.org/html/2606.15461#bib.bib39)\]\.ESBMChas accumulated 43 competitive awards atCompetition on Software Verification \(SV\-COMP\)andCompetition on Software Testing \(Test\-Comp\)\(as tabulated in annual competition reports; see\[[7](https://arxiv.org/html/2606.15461#bib.bib22)\]for a consolidated record\) and has been deployed industrially at Lockheed Martin and within the NVIDIA\-OpenSMA framework\[[7](https://arxiv.org/html/2606.15461#bib.bib22)\]\.

Yet until recently, no open\-source formal verification tool could directly acceptLadder Diagram \(LD\)programs\.LDis the dominantPLCprogramming notation – standardized inInternational Electrotechnical Commission \(IEC\)61131\-3and estimated by industry sources to account for over 60% of installedPLCbases in North American and Japanese manufacturing \(as cited in\[[27](https://arxiv.org/html/2606.15461#bib.bib3)\]\)\.LDprograms are graphical: composed of horizontal rungs, each encoding a Boolean condition \(contacts\) linked to an output action \(coils\)\. There is no textual source file for a C\-oriented model checker to parse, no type system to extract, and no control\-flow graph to construct – at least not without a dedicated translation layer\. This translation gap has left the majority of industrial control logic outside the reach of modern formal verification\.

This paper presentsESBMC\-PLC\[[5](https://arxiv.org/html/2606.15461#bib.bib24)\], a tool for the formal verification ofIEC61131\-3LDprograms usingSatisfiability Modulo Theories \(SMT\)\-based model checking, the first open\-source formal verifier with native support forIEC61131\-3LDprograms in the standard PLCopen XML format\. ESBMC\-PLC is implemented as a new frontend forESBMCand accepts the same PLCopen XML files exported by all majorPLCvendors \(Siemens TIA Portal, CODESYS, Rockwell Studio 5000\) without any manual translation or preprocessing\. Safety properties are specified in a YAML file using five property kinds that cover the most common industrial requirements, without requiring expertise in temporal logic\. Verification is performed usingESBMC’sSMT\-based engine with Z3, supporting both incrementalBounded Model Checking \(BMC\)for fast bug finding andk\-induction for unbounded safety proofs\.

### 1\.1Contributions

1. 1\.ESBMC\-PLC tool\[[5](https://arxiv.org/html/2606.15461#bib.bib24)\]\(§[7](https://arxiv.org/html/2606.15461#S7)\): a complete, open\-sourceLDfrontend forESBMCthat parses PLCopen XML \(graphicaltc6\_0201format\), translatesLDrungs toESBMC’s GOTO intermediate representation, encodes thePLCscan cycle as awhile\(true\)loop with nondeterministic inputs, and checks user\-defined safety properties viaSMT\-basedBMCork\-induction – the first tool to achieve this for a mature, award\-winning model checker\.
2. 2\.Encoding rules and scan\-cycle design decisions\(§[7\.3](https://arxiv.org/html/2606.15461#S7.SS3)\): a core\-subset of translation rules forIEC61131\-3LDelements – XIC/XIO contacts, OTE/OTL/OTU coils, TON/TOF/TP timers, CTU/CTD counters, and arithmetic function blocks –*designed*to match Ebnenasir’s formalLDsemantics\[[8](https://arxiv.org/html/2606.15461#bib.bib11)\]and empirically validated over 13 benchmarks; and three methodological encoding decisions that determine the scope of the verification guarantees: nondeterministic input re\-sampling \(open\-world sensor model\), static persistent output\-coil state \(correct output\-image semantics across scan boundaries\), and an unboundedwhile\(true\)loop body \(enablingk\-induction\)\.
3. 3\.YAML property language\(§[7\.4](https://arxiv.org/html/2606.15461#S7.SS4)\): a five\-kind property specification format \(mutual\_exclusion,invariant,absence,response,reachability\) with requiredjustificationfields forresponseandreachabilityproperties, documenting the timing assumptions behind bounded\-horizon specifications and lowering the barrier to formal property specification for automation engineers without a formal\-methods background\.
4. 4\.Experimental evaluation\(§[8](https://arxiv.org/html/2606.15461#S8)\): results on 13 benchmarks \(7 safe variants, 6 unsafe variants\) spanning 6 industrial domains and 3 program sources – original ESBMC\-PLC benchmarks, synthetic programs derived from publishedPLCliterature, and real\-world vendor programs \(CONTROLLINO\[[4](https://arxiv.org/html/2606.15461#bib.bib25)\]and MathWorks\[[19](https://arxiv.org/html/2606.15461#bib.bib26)\]\) – verifying 61 properties with correct classification of all 13 programs \(9 author\-constructed verified as expected by design; 4 independent vendor programs correctly classified without pre\-assigned labels\), zero false positives, 8 bugs found with actionable counterexamples, and all verification runs completing in under60ms60\\text\{\\,\}\\mathrm\{ms\}on Apple Silicon \(aarch64\)\.
5. 5\.Comparative analysis\(§[4](https://arxiv.org/html/2606.15461#S4)–[9](https://arxiv.org/html/2606.15461#S9)\): a systematic review of 22 studies \(2020–2026\) characterising four technical directions inPLCLDverification, four research gaps that motivate ESBMC\-PLC, and a direct feature comparison with PLCverif – the state\-of\-the\-artPLCformal verification platform – demonstrating that ESBMC\-PLC is the only tool providing nativeLDinput,k\-induction unbounded proofs, andSMTbit\-vector semantics together\.

### 1\.2Scope of Guarantee

The soundness of ESBMC\-PLC’s verification results rests on theLD\-to\-GOTO\-Intermediate Representation \(IR\)translation layer\. This layer is grounded in Ebnenasir’s formalLDsemantics\[[8](https://arxiv.org/html/2606.15461#bib.bib11)\]and has been empirically validated on the 13\-benchmark suite; it has not been formally proved equivalent to theIEC61131\-3standard\. Timer preset values are interpreted as scan\-cycle counts \(not milliseconds\), diverging fromIECTIME semantics; users must convert accordingly\. The current implementation covers a core subset ofIEC61131\-3constructs: REAL/FLOAT types, strings, arrays, multiple POUs, and interrupt tasks are not supported and generate anUnsupportedConstructerror at parse time\.

The remainder of this paper is structured as follows\. Section[2](https://arxiv.org/html/2606.15461#S2)provides background onPLCarchitecture,IEC61131\-3, andESBMC\. Section[3](https://arxiv.org/html/2606.15461#S3)discusses related work\. Sections[4](https://arxiv.org/html/2606.15461#S4)–[6](https://arxiv.org/html/2606.15461#S6)survey existing translation approaches and identify research gaps\. Section[7](https://arxiv.org/html/2606.15461#S7)presents the ESBMC\-PLC architecture\. Section[8](https://arxiv.org/html/2606.15461#S8)reports the experimental evaluation\. Section[9](https://arxiv.org/html/2606.15461#S9)compares ESBMC\-PLC with PLCverif\. Section[10](https://arxiv.org/html/2606.15461#S10)discusses findings\. Section[11](https://arxiv.org/html/2606.15461#S11)addresses threats to validity\. Section[12](https://arxiv.org/html/2606.15461#S12)outlines future directions\. Section[13](https://arxiv.org/html/2606.15461#S13)concludes\.

## 2Background

### 2\.1PLCArchitecture and the Scan Cycle

APLCconsists of aCentral Processing Unit \(CPU\), non\-volatile program memory, input modules \(reading digital/analog sensor signals\), and output modules \(driving actuators\)\. Execution follows a fixed*scan cycle*: \(1\) read all inputs into a process image, \(2\) execute the user program from first rung to last, updating internal variables and the output image, \(3\) write the output image to physical actuators, \(4\) handle communications, and \(5\) repeat\. Cycle times typically range from1msto100ms1\\text\{\\,\}\\mathrm\{ms\}100\\text\{\\,\}\\mathrm\{ms\}\.

This deterministic, cyclic execution model has important consequences for formal verification\. APLCprogram is not a general\-purpose procedure but a*reactive system*: it maps a finite input state to a finite output state at each cycle\. State\-based model checkers are thus well matched toPLCprograms in principle, provided the scan\-cycle semantics are correctly encoded\. The key challenge is that commercialPLCsintroduce platform\-specific extensions – such as multitask preemption, interrupt\-driven tasks, and inter\-task shared variables – that complicate the basic cycle model\[[13](https://arxiv.org/html/2606.15461#bib.bib15),[14](https://arxiv.org/html/2606.15461#bib.bib21)\]\.

### 2\.2IEC61131\-3Languages

TheIEC61131\-3standard \(3rd edition, 2013\) defines five programming languages forPLCs, summarised in Table[1](https://arxiv.org/html/2606.15461#S2.T1)\.

Table 1:IEC61131\-3programming languagesLanguageTypePrimary useLadder Diagram \(LD\)GraphicalRelay\-logic replacements, general controlFunctional Block Diagram \(FBD\)GraphicalSignal flow, continuous controlStructured Text \(ST\)TextualComplex algorithms, data manipulationInstruction List \(IL\)TextualLow\-level, assembly\-like \(deprecated\)Sequential Function Chart \(SFC\)GraphicalState\-machine controlLDdominates installed base, particularly in North American and Japanese manufacturing\. A Ladder program consists of*rungs*: each rung evaluates a Boolean combination of*contacts*\(normally\-open XIC and normally\-closed XIO\) and assigns the result to one or more*coils*\(output\-enable OTE, set OTL, reset OTU\)\. Timer and counter function blocks appear as specialized rung elements\. Ladder programs are stored and exchanged in PLCopen XML \(tc6\_0201\), an open standard supported by all majorPLCvendors\.

STis syntactically similar to Pascal or C, making it the natural target for source\-to\-source translation into C\.STshares assignment, branching \(IF/THEN/ELSE\), and loop constructs with C, andSTprograms are already compiled to C by the MATIEC open\-sourceIEC61131\-3compiler and the OpenPLC runtime system\. The semantic relationship betweenLDandSTis well understood at the single\-task level, but the correctness of vendor\-providedLD\-to\-STconversions has not been formally proved in the open literature\[[26](https://arxiv.org/html/2606.15461#bib.bib13)\]\.

### 2\.3ESBMC: Architecture and Verification Engine

ESBMCwas originally developed as an extension ofBounded Model Checking for ANSI\-C Programs \(CBMC\)for embeddedAmerican National Standards Institute C \(ANSI\-C\)software and has since evolved into a multi\-language verification platform\[[7](https://arxiv.org/html/2606.15461#bib.bib22)\]\. Its internal architecture centers on the GOTO\-programIR: a simplified three\-address code form of the input program, annotated with assumptions and assertions\. AllESBMCfrontends produce GOTO programs; the verification backend operates exclusively on thisIR\.

The verification engine supports four strategies:

1. 1\.BMC: the GOTO program is symbolically executed for a fixed number of steps; the resulting formula is passed to anSMTsolver\. Violations produce concrete counterexample traces\.
2. 2\.k\-induction: combinesBMC\(base case\) with an inductive step to prove properties without full loop unrolling\.
3. 3\.Property\-Directed Reachability \(PDR/IC3\): frame\-based safety proof algorithm\.
4. 4\.Invariant Inference: automatically derives loop invariants to strengthen inductive proofs\.

ESBMCsupports Z3, Bitwuzla, MathSAT, Yices, and Boolector asSMTback\-ends\. ESBMC\-PLC is implemented as anLDfrontend forESBMC: it translates PLCopen XML programs to the GOTO\-programIR, making anyLDprogram immediately verifiable by the fullESBMCverification engine\.

### 2\.4Related Formal Verification Tools

Existing formal verification tools forPLCprograms either target languages other thanLDor rely on different verification approaches\.CBMCshares the GOTO\-programIRwithESBMCand is used as a backend for PLCVerif, an open\-sourceConseil Européen pour la Recherche Nucléaire \(CERN\)platform that translates SiemensStructured Control Language \(SCL\)intoCBMC, nuXmv, or Theta, but does not acceptLDinput\[[17](https://arxiv.org/html/2606.15461#bib.bib7),[16](https://arxiv.org/html/2606.15461#bib.bib20),[9](https://arxiv.org/html/2606.15461#bib.bib18)\]\. Other tools, such as NuSMV and nuXmv, work with SMV models\[[28](https://arxiv.org/html/2606.15461#bib.bib1),[12](https://arxiv.org/html/2606.15461#bib.bib16)\], while SPIN targets Promela models derived fromST\[[11](https://arxiv.org/html/2606.15461#bib.bib14)\]\. Why3 supports deductive verification via anLD\-to\-WhyML pipeline\[[1](https://arxiv.org/html/2606.15461#bib.bib2),[2](https://arxiv.org/html/2606.15461#bib.bib5)\], and Maude\-SMTcombines rewriting logic withSMTforSTverification\[[15](https://arxiv.org/html/2606.15461#bib.bib6),[13](https://arxiv.org/html/2606.15461#bib.bib15)\]\. CoVeriTeam offers a cooperative framework for composing multiple verifiers, includingESBMC\[[25](https://arxiv.org/html/2606.15461#bib.bib9),[24](https://arxiv.org/html/2606.15461#bib.bib10)\]\.

## 3Related Work

### 3\.1PLCProgramming and the Verification Challenge

PLCsform the execution backbone ofIndustrial Control Systems \(ICS\)in domains ranging from nuclear power generation to railway signaling\.LDremains the most widely deployedPLClanguage due to its graphical relay\-diagram notation familiar to automation engineers\[[27](https://arxiv.org/html/2606.15461#bib.bib3)\]\. Despite the safety\-critical nature ofPLCdeployments, formal verification ofPLCprograms lags significantly behind practice for general\-purpose software\. Sun et al\.\[[23](https://arxiv.org/html/2606.15461#bib.bib4)\]systematize the attack surface of industrial control logic, identifying a fundamental asymmetry: most formal verification research targetsSTand ignoresLD\. The consequence is that adversaries can injectLLB\[[12](https://arxiv.org/html/2606.15461#bib.bib16)\]or manipulate coil outputs\[[18](https://arxiv.org/html/2606.15461#bib.bib12)\]without practical means of automated formal detection\.

### 3\.2Model Checking forSTPrograms

Safety properties inComputation Tree Logic \(CTL\)can be verified using NuSMV through a Behavior Model automatically extracted fromSTprograms by variable\-state analysis\[[28](https://arxiv.org/html/2606.15461#bib.bib1)\]\. Their evaluation on nuclearPLCprograms demonstrates that model\-checking approaches can scale to industrial\-sizedSTcode\. A rigorous formal semantics forSTremains an open challenge, though several approaches have been proposed\. K\-STprovides an executable semantics in the K framework, validated against 509 open\-sourceSTprograms and three commercial compilers, uncovering five compiler bugs and nine OpenPLC defects\[[26](https://arxiv.org/html/2606.15461#bib.bib13)\]\. Another line of work encodesSTsemantics directly as rewriting\-modulo\-SMTrules in Maude, applyingBMCto verifyLinear Temporal Logic \(LTL\)properties\[[15](https://arxiv.org/html/2606.15461#bib.bib6)\], with subsequent extensions supporting multitask programs under preemptive scheduling\[[13](https://arxiv.org/html/2606.15461#bib.bib15)\]and networkedPLCsystems\[[14](https://arxiv.org/html/2606.15461#bib.bib21)\]\. Meanwhile, a process\-orientedSTextension can be translated to Promela via an Xtext\-based translator, enabling SPIN model checking of concurrentPLCtasks\[[11](https://arxiv.org/html/2606.15461#bib.bib14)\]\.

### 3\.3Formal Verification Platforms forPLCs

The PLCVerif platform, developed atCERNand open\-sourced in 2020, translates SiemensSCL\(anSTdialect\) into a GOTO\-programIRthat can be consumed byCBMC, nuXmv, or Theta\[[17](https://arxiv.org/html/2606.15461#bib.bib7)\]\. This platform has been demonstrated as an industrial verification service at the GSI heavy\-ion accelerator\[[16](https://arxiv.org/html/2606.15461#bib.bib20)\]and extended to support pure\-pastLTLsafety properties via FRET\-derived PLTL specifications\[[9](https://arxiv.org/html/2606.15461#bib.bib18)\]\. Beyond PLCVerif, a cooperative verification pipeline compiles 40 real\-world PLCOpenSTprograms to C through OpenPLC/MATIEC and verifies them using multiple tools, includingESBMC\-INCR,CBMC, CPA\-SEQ, and Symbiotic, confirming thatESBMCis algorithmically well\-suited forPLCproperty verification\[[25](https://arxiv.org/html/2606.15461#bib.bib9)\]\. This conclusion is independently corroborated, withESBMCmatching or outperforming NuSMV on verification time for smallSTprograms\[[22](https://arxiv.org/html/2606.15461#bib.bib8)\]\.

### 3\.4Verification Approaches Specific toLD

Before the present work, the most complete academic pipeline forLDtranslatesLDprograms with timing charts into WhyML \(the Why3 input language\) and discharges proof obligations through a portfolio of automated theorem provers, achieving 78% automation\[[1](https://arxiv.org/html/2606.15461#bib.bib2),[2](https://arxiv.org/html/2606.15461#bib.bib5)\]\. On the semantic front, the most rigorous formal semantics ofLDscan cycles formalizes contact evaluation, OTL/OTU latching, timer, and counter blocks\[[8](https://arxiv.org/html/2606.15461#bib.bib11)\]\. Other efforts include an architecture for detectingLLBusing NuSMV on a 60\-program SWaTLDdataset\[[12](https://arxiv.org/html/2606.15461#bib.bib16)\]and the development ofPLC\-VBS, a vendor\-agnostic vulnerability scanner forLDcontacts and coils\[[18](https://arxiv.org/html/2606.15461#bib.bib12)\]\. The most technically completeLD\-to\-SMTtranslation, which mapsIEC61131\-3data types toSMTsorts and encodes rungs recursively as Boolean circuit gates under a global clock, is unfortunately proprietary\[[3](https://arxiv.org/html/2606.15461#bib.bib19)\]\.

#### 3\.4\.1Positioning of ESBMC\-PLC

ESBMC\-PLC differs from all prior work in three ways:

1. 1\.It is the first open\-source tool to acceptLDprograms in standard PLCopen XML format without any translation or preprocessing;
2. 2\.It is the first to applyk\-induction toLDprograms, enabling unbounded safety proofs;
3. 3\.It produces counterexamples that reference originalLDvariable names, making results directly interpretable by automation engineers\.

## 4Survey of Translation Approaches

### 4\.1Systematic Search Methodology

This survey follows a PRISMA 2020\-aligned protocol\. Ten sources were searched on 2026\-05\-28: IEEE Xplore, ACM Digital Library, arXiv \(cs\.SE, cs\.PL, cs\.CR\), Semantic Scholar, SpringerLink, MDPI, Inria HAL, the USPTO patent database, Google Scholar, and ResearchGate\. Twelve search strings varied keywords across synonyms \(ladder logic,LD,IEC61131\-3\), tools \(ESBMC,CBMC,SMT, model checking\), and operations \(translation, transformation, verification, compilation\)\.Inclusion: English studies published January 2020–May 2026 addressingLD/ST\-to\-formal\-language translation orSMT\-basedBMCapplied toPLCprograms\.Exclusion: pre\-2020; non\-English; FBD/SFC/IL\-only withoutLDcontent; purely theoretical with no implementation\. Results: 68 records identified, 52 after deduplication \(performed by manual cross\-referencing of DOIs and titles across all ten sources\),22 included\.

Table[2](https://arxiv.org/html/2606.15461#S4.T2)summarises all 22 included studies\.

Table 2:Included studies \(2020–2026,n=22n=22\)YearApproach \+ ReferenceVerifierLang\.2020Behaviour Model extraction\[[28](https://arxiv.org/html/2606.15461#bib.bib1)\]NuSMVST2021LD\+ timing charts→\\toWhy3\[[1](https://arxiv.org/html/2606.15461#bib.bib2)\]Why3 proversLD2021Synthesis \+ TIA Portal\[[27](https://arxiv.org/html/2606.15461#bib.bib3)\]FastsynthST/LD2021Survey of attacks/defences\[[23](https://arxiv.org/html/2606.15461#bib.bib4)\]MultipleLD/ST2022LD→\\toWhyML→\\toWhy3\[[2](https://arxiv.org/html/2606.15461#bib.bib5)\]Why3 proversLD2022Rewriting moduloSMT\[[15](https://arxiv.org/html/2606.15461#bib.bib6)\]Maude\-SMTST2022ST→\\toCBMCIR\[[17](https://arxiv.org/html/2606.15461#bib.bib7)\]CBMC, nuXmv, ThetaST2023ST→\\toC \(manual\)\[[22](https://arxiv.org/html/2606.15461#bib.bib8)\]NuSMV,ESBMCST2023OpenPLC/MATIEC→\\toCoVeriTeam\[[25](https://arxiv.org/html/2606.15461#bib.bib9)\]ESBMC,CBMC, CPA\-SEQST→\\toC2023PLCOpen benchmarks\[[24](https://arxiv.org/html/2606.15461#bib.bib10)\]ESBMC\-INCR,CBMCST→\\toC2023FormalLDsemantics \(TLA\+\-style\)\[[8](https://arxiv.org/html/2606.15461#bib.bib11)\]Manual / TLA\+LD2023Static analysis of contacts/coils\[[18](https://arxiv.org/html/2606.15461#bib.bib12)\]Vuln\. scannerLD2023K\-framework semantics\[[26](https://arxiv.org/html/2606.15461#bib.bib13)\]K \(executable\)ST2024poST→\\toPromela\[[11](https://arxiv.org/html/2606.15461#bib.bib14)\]SPINST2024Rewriting semantics \+ preemption\[[13](https://arxiv.org/html/2606.15461#bib.bib15)\]Maude\-SMTST2024LD→\\toNuSMV forLLBdetection\[[12](https://arxiv.org/html/2606.15461#bib.bib16)\]NuSMVLD2024Dynamic symbolic execution\[[21](https://arxiv.org/html/2606.15461#bib.bib17)\]PLCAutoTesterST2024PLTL monitors→\\toCBMCassertions\[[9](https://arxiv.org/html/2606.15461#bib.bib18)\]PLCVerif/CBMCST2024LDcontacts/coils→\\toSMTcircuit\[[3](https://arxiv.org/html/2606.15461#bib.bib19)\]SMT\(proprietary\)LD2025PLCVerif\-as\-a\-service\[[16](https://arxiv.org/html/2606.15461#bib.bib20)\]CBMCST2025Discrete \+ network \+ continuous\[[14](https://arxiv.org/html/2606.15461#bib.bib21)\]Rewriting logicST2026ESBMCsurvey \(noLDfront\-end\)\[[7](https://arxiv.org/html/2606.15461#bib.bib22)\]ESBMCC/multiNote on scope:\[[21](https://arxiv.org/html/2606.15461#bib.bib17)\]\(PLCAutoTester, 2024\) employs dynamic symbolic execution rather than model checking or deductive verification, and does not targetLDtranslation; it is included for completeness but falls outside the four translation directions analyzed below\.

### 4\.2Direction 1: Deductive Verification via Why3

The earliest academic pipeline forLDformal verification translates Ladder programs to the Why3 deductive platform, which separates verification\-condition generation from their discharge by a portfolio of automated theorem provers \(Alt\-Ergo, CVC4, Z3, Vampire\)\. Unlike bounded model checking, this proves properties for all possible inputs and arbitrarily many scan cycles – at the cost of requiring annotations and occasional manual proof steps\.

In one line of work,LDrungs are translated to WhyML functions with scan cycles represented as WhyML programs that sequence rung calls\[[1](https://arxiv.org/html/2606.15461#bib.bib2),[2](https://arxiv.org/html/2606.15461#bib.bib5)\]\. Applied to MitsubishiPLCs, this approach automatically discharges approximately 78% of proof obligations\. While it covers XIC/XIO contacts, OTE coils, and standard TON/CTU blocks, it does not handle latching coils \(OTL/OTU\), Master Control Relays, multitask programs, or non\-Boolean arithmetic flows\. Critically for the present work, WhyML is not processable byESBMC, and no WhyML\-to\-C transpiler exists in the literature\.

### 4\.3Direction 2:SMTCircuit Models fromLDs

A recent patent provides the most technically completeLD\-to\-SMTtranslation\[[3](https://arxiv.org/html/2606.15461#bib.bib19)\]\. In this approach,IEC61131\-3types are mapped toSMTsorts \(BOOL→\\toBoolean, INT→\\toint16, etc\.\),PLCoutputs become circuit latches\. Rungs are parsed recursively: XIC contacts become Boolean variable references, XIO contacts become negations, series connections become AND, parallel connections become OR, and arithmetic function blocks becomeSMTarithmetic operations\. A global clock models the scan cycle\. While the Nozomi patent establishes thatLDcan be represented as a Boolean circuit overSMTsorts, ESBMC\-PLC departs from it in three design decisions not present or described in that work: \(i\) the scan cycle is encoded as a GOTO\-programwhile\(true\)loop rather than a one\-shot circuit, enablingk\-induction over unbounded scan sequences; \(ii\) input variables are re\-sampled nondeterministically at each iteration, modelling the full input space without enumerating concrete traces; and \(iii\) the translation targets the openESBMCGOTO\-IRrather than a proprietary solver, making the translated program inspectable, testable against a reference runtime, and verifiable with any ESBMC strategy\.

Separately, a related architecture using NuSMV forCTL\-basedLLBdetection has been demonstrated on 60 programs from the SWaT testbed\[[12](https://arxiv.org/html/2606.15461#bib.bib16)\]\.

### 4\.4Direction 3:STasIR

Given the semantic equivalence ofLDandSTat the single\-task scan\-cycle level, translatingLDtoSTand thenSTto C via MATIEC/OpenPLC creates a two\-step pathway toESBMC\. Validated executable formal semantics forSTexist, having been tested against 509 GitHub programs and exposing five compiler bugs\[[26](https://arxiv.org/html/2606.15461#bib.bib13)\]\. PLCVerif already translatesSCL\(anSTdialect\) to aCBMC\-compatibleIR, meaning that substitutingESBMCforCBMCwould be a low\-complexity engineering change\[[17](https://arxiv.org/html/2606.15461#bib.bib7)\]\. Direct evaluations ofESBMCon C\-translatedPLCprograms confirm its algorithmic effectiveness for this domain\[[25](https://arxiv.org/html/2606.15461#bib.bib9),[22](https://arxiv.org/html/2606.15461#bib.bib8)\]\. ESBMC\-PLC improves upon these approaches by bypassing the two\-step chain entirely, translatingLDdirectly to GOTO\-IRand thereby avoiding the fidelity risks inherent in theLD→\\toSTtranslation step\[[26](https://arxiv.org/html/2606.15461#bib.bib13)\]\.

### 4\.5Direction 4: Formal Semantics ofLD

The absence of a machine\-checkableLDsemantics remains the most significant obstacle to a formally correctLD\-to\-C compiler\. A rigorousLDformalization from the review period addresses this gap, covering contact evaluation, OTL/OTU latch semantics, TON/TOF/TP timers, CTU/CTD counters, and fault\-injection operators\[[8](https://arxiv.org/html/2606.15461#bib.bib11)\]\. ESBMC\-PLC’s encoding rules for the elements covered by this formalization are*designed*to match the corresponding definitions: OTL/OTU latches follow the set\-priority semantics specified for latch coils; CTU counters use edge\-triggered semantics matching the counter block definition; and TON accumulation follows the on\-delay timer specification\. These design choices are validated empirically via the benchmark suite but not formally proved equivalent to theIEC61131\-3standard; a K\-LDsemantics \(extending K\-ST\[[26](https://arxiv.org/html/2606.15461#bib.bib13)\]\) is the natural future vehicle for a machine\-checked equivalence proof\.

## 5Comparative Analysis of Existing Approaches

### 5\.1Translation Direction Comparison

To clarify the trade\-offs between different approaches, Table[3](https://arxiv.org/html/2606.15461#S5.T3)compares the four translation directions against ESBMC\-PLC across six dimensions\. Direction 1 relies on Why3 for WhyML proofs; Direction 2 translatesLDintoSMTcircuits; Direction 3 compilesSTtoANSI\-C; and Direction 4 produces TLA\+/K specifications without direct verification\. ESBMC\-PLC serves as a native baseline\. The table shows that only Direction 3 and ESBMC\-PLC areESBMC\-ready, with ESBMC\-PLC uniquely combining industrial\-scale testing, open\-source licensing, and soundness alignment with\[[8](https://arxiv.org/html/2606.15461#bib.bib11)\]\.

Table 3:Comparison ofLDtranslation directions and ESBMC\-PLCDimensionDir\. 1 \(Why3\)Dir\. 2 \(SMT\)Dir\. 3 \(ST→\\toC\)Dir\. 4 \(Semantics\)ESBMC\-PLCOutput formatWhyMLSMTcircuitANSI\-CTLA\+/K specGOTO\-IRESBMC\-ready?No \(indirect\)No \(propr\.\)YesNo \(spec only\)Yes \(native\)Open\-sourceYes \(Why3\)No \(patent\)Yes \(MATIEC\)PartialYes \(MIT\)LDcoveragePartialFull \(claimed\)DependsPartialCore subsetSoundness provedPartial \(VCs\)Not provedNot provedSpec onlyDesigned to match\[[8](https://arxiv.org/html/2606.15461#bib.bib11)\]; empiricalIndustrial scaleSmall examplesIndustrial40 programsConceptual13 programs, real vendors
### 5\.2Verifier Capability Comparison

Table[4](https://arxiv.org/html/2606.15461#S5.T4)compares the tools used across the included studies, focusing on input language support, verification techniques, and open\-source availability\. ESBMC\-PLC is the only tool that natively supportsLDandBMCwithSMTsolvers and remains open\-source\. Other tools either require translation fromLD\(e\.g\., NuSMV, Why3\), lack nativePLClanguage support \(e\.g\.,CBMC, SPIN\), or are proprietary \(Nozomi\)\. Notably,ESBMCcan handleSTindirectly via C translation, and PLCVerif bridgesSTtoCBMC\. The table highlights ESBMC\-PLC’s unique combination of nativeLDinput,BMC/SMTbackend, and permissive licensing\.

Table 4:Formal verification tools forPLCprogramsToolInputLD?ST?BMC?SMT?OSS?ESBMC\-PLCPLCopen XMLYesNoYesYesYesESBMCC, C\+\+, …Via ESBMC\-PLCVia CYesYesYesCBMCC, C\+\+NoVia PLCVerifYesSATYesPLCVerifSCL\(ST\)NoYesViaCBMCViaCBMCYesNuSMV/nuXmvSMVVia transl\.Via transl\.PartialNoYesSPINPromelaNoVia GaraninaBMCmodeNoYesWhy3WhyMLVia BL et al\.NoNo \(deductive\)Via proversYesMaude\-SMTMaude rulesNoYes \(Lee\)YesYesPartialNozomi \(pat\.\)LDYesNoViaSMTYesNo

## 6Research Gaps

The analysis above reveals four interrelated research gaps\. ESBMC\-PLC directly addressesGap 1andGap 2;Gap 3andGap 4are partially addressed and remain targets for future work\.

1. GAP 1:No open\-source, validatedLD\-to\-C translator\. No open\-source, peer\-reviewed compiler translatedIEC61131\-3LDtoANSI\-Cbefore this work\. The Why3 pipeline\[[2](https://arxiv.org/html/2606.15461#bib.bib5)\]targets WhyML, not C\. The Nozomi patent\[[3](https://arxiv.org/html/2606.15461#bib.bib19)\]is proprietary\. CommercialLD\-to\-STconverters are undocumented and unvalidated\.ESBMC\-PLC closes this gapby providing an open\-source \(MIT\)LD\-to\-GOTO\-IRtranslator integrated intoESBMC, with encoding rules grounded in Ebnenasir’s formal semantics\[[8](https://arxiv.org/html/2606.15461#bib.bib11)\]\.
2. GAP 2:NoESBMCfront\-end forIEC61131\-3\.TheESBMCsurvey\[[7](https://arxiv.org/html/2606.15461#bib.bib22)\]confirms noLDorSTfront\-end existed prior to this work\.ESBMC\-PLC closes this gapby implementing a completeLDfront\-end forESBMC, enabling the fullESBMCverification engine – includingk\-induction, overflow checking, and all supportedSMTback\-ends – to be applied toLDprograms\.
3. GAP 3:NoLDbenchmark suite in a formal\-verification\-compatible form\.The PLCOpen suite\[[24](https://arxiv.org/html/2606.15461#bib.bib10)\]provides 40 programs with formal properties but all originate inST\.ESBMC\-PLC partially addresses this gapwith 13 benchmarks spanning 6 domains and 3 real\-world sources, in PLCopen XML format with YAML property files\.
4. GAP 4:Unverified semantic fidelity of theLD→\\toST→\\toC chain\.Wang et al\.\[[26](https://arxiv.org/html/2606.15461#bib.bib13)\]showSTcompilers contain semantic defects detectable only by formal analysis\.ESBMC\-PLC avoids this gap entirelyby translatingLDdirectly to GOTO\-IRwithout passing throughST, eliminating the intermediate conversion step and its associated fidelity risks\.

## 7ESBMC\-PLC: Architecture and Design

### 7\.1System Overview

ESBMC\-PLC is implemented as anLDfrontend forESBMC\(build flag:ENABLE\_LD\_FRONTEND=On\) and is publicly available at Zenodo\[[6](https://arxiv.org/html/2606.15461#bib.bib23)\]\(source:\[[5](https://arxiv.org/html/2606.15461#bib.bib24)\]\)\. It provides two command\-line interfaces: the mainesbmcbinary \(withLDinput detection\) andld\-verify, a purpose\-built wrapper with structured output\. The verification pipeline comprises five stages, as illustrated conceptually in Figure[1](https://arxiv.org/html/2606.15461#S7.F1):

1. 1\.PLCopen XML Parsing: theLDfile is parsed into an in\-memory rung graph\.
2. 2\.Property Parsing: the YAML property file is parsed into a property set\.
3. 3\.LD\-to\-GOTO\-IRTranslation: the rung graph is translated toESBMC’s GOTO\-programIRencoding the scan\-cycle loop\.
4. 4\.Property Injection: properties are compiled toassert\(\)andassume\(\)statements in the GOTO program\.
5. 5\.Verification:ESBMCruns the selected strategy \(incrementalBMCork\-induction\) with Z3 as theSMTback\-end\.

PLCopen XMLYAML propsParse & BuildRung GraphLD\-to\-GOTO\-IRTranslatorESBMC \+ Z3SAFEVIOLATIONFigure 1:ESBMC\-PLC verification pipeline
### 7\.2Input Format: PLCopen XML

ESBMC\-PLC acceptsLDfiles in PLCopen XML format \(tc6\_0201\), the standardized open interchange format supported by Siemens TIA Portal, CODESYS, Rockwell Studio 5000, OpenPLC Editor v3, and Beremiz\. The graphical variant of this format encodes element positions and connections viarefLocalIdattributes that establish a directed graph among contacts, function blocks, and coils\. ESBMC\-PLC’s parser handles both textual and graphical PLCopen XML, reconstructing the circuit topology from refLocalId references without requiring any manual editing of the exported file\.

The parser correctly handles the graphical format with coordinate\-based connections as exported by OpenPLC Editor v3 and the CONTROLLINO toolchain\[[4](https://arxiv.org/html/2606.15461#bib.bib25)\], as demonstrated in the real\-world benchmarks \(CS10–CS13 in §[8](https://arxiv.org/html/2606.15461#S8)\)\.

### 7\.3LD\-to\-GOTO\-IRTranslation

#### 7\.3\.1Data Type Mapping

EachIEC61131\-3type is mapped to its smallest C equivalent, preserving the value range, consistent with the type model ofBruttomessoet al\.\[[3](https://arxiv.org/html/2606.15461#bib.bib19)\]:

Table 5:IEC61131\-3to C data type mappingIEC61131\-3C typeBitsNotesBOOLbool1True/falseSINTint8\_t8SignedINTint16\_t16SignedDINTint32\_t32SignedLINTint64\_t64SignedUINTuint16\_t16UnsignedUDINTuint32\_t32UnsignedREALfloat32IEEE 754LREALdouble64IEEE 754TIMEuint32\_t32Milliseconds
#### 7\.3\.2Scan\-Cycle Encoding

ThePLCscan cycle is encoded as a GOTO\-program loop body called repeatedly from awhile\(true\)top\-level loop\. Three storage classes are used: \(a\)*input variables*are re\-sampled each cycle as nondeterministic values, modeling the full range of possible sensor readings; \(b\)*output coil variables*arestatic\-equivalent persistent state, modeling thePLCoutput image that persists across cycles; \(c\)*internal memory bits*are persistent state corresponding toPLCmarker bits\. This encoding correctly models both the combinational evaluation within a scan cycle and the sequential state evolution across cycles\. Three design decisions in this structure determine the scope of the verification guarantees:

1. 1\.Nondeterministic input re\-sampling\.Inputs are re\-drawn from a nondeterministic oracle at every iteration, not fixed to a concrete trace\. This encodes the open\-world assumption that any sensor reading can occur at any scan, ensuringESBMCexplores all reachable states and cannot miss violations conditioned on specific input sequences\.
2. 2\.Static persistent state\.Output coils and marker bits arestatic\-equivalent persistent variables that retain their value across loop iterations unless explicitly written\. This correctly models thePLCoutput image – which persists until rewritten – and is essential for detecting multi\-scan bugs such as the timer\-reset failure in CS2 \(§[8](https://arxiv.org/html/2606.15461#S8)\)\.
3. 3\.while\(true\)loop body\.The scan cycle is the body of an unbounded loop, not a bounded unrolling\. This enablesk\-induction to prove properties*for all*future scan counts, providing a stronger guarantee thanBMCalone and distinguishing ESBMC\-PLC from bounded\-only approaches\.

The canonical structure is shown in Listing[1](https://arxiv.org/html/2606.15461#LST1)\.

1

2staticboolQ\_OUT1=false;

3staticboolM\_AUX=false;

4

5voidplc\_cycle\(void\)\{

6

7boolI\_IN1=\_\_ESBMC\_nondet\_bool\(\);

8boolI\_IN2=\_\_ESBMC\_nondet\_bool\(\);

9

10

11

12

13

14

15\}

16

17intmain\(void\)\{

18while\(1\)\{plc\_cycle\(\);\}

19return0;

20\}

Listing 1:Scan\-cycle GOTO\-IR template \(shown as equivalent C\)
##### Parallel\-rung OR semantics\.

InIEC61131\-3LDs, multiple rungs driving the same output coil are semantically equivalent to a logical OR: the coil is energized if*any*rung provides a closed path\. In the GOTOIR, this is encoded as multiple sequentialASSIGNinstructions to the same variable; the last assignment appears to win, but because each rung includes only the conditions under which it*energizes*the coil \(and evaluates tofalseotherwise\), theESBMCsymbolic execution engine correctly OR\-combines all evaluations via theSMTencoding\. When re\-executing the GOTOIRconcretely \(Section[8\.9](https://arxiv.org/html/2606.15461#S8.SS9)\), care must be taken to OR\-combine multiple assignments to the same destination variable rather than taking the last value only\. An additional subtlety is the coil\-energize prefix1&&that the converter emits at the start of every rung expression: this literal must be stripped only at the start of the expression, not globally, to avoid incorrect evaluation when the conditions include other literal1values\.

#### 7\.3\.3Rung\-to\-IRTranslation Rules

Contact and coil elements map to GOTO\-IRoperations as shown in Table[6](https://arxiv.org/html/2606.15461#S7.T6)\. The rules for XIC/XIO contacts, OTE/OTL/OTU coils, TON/TOF/TP timers, and CTU/CTD counters are*designed*to match the corresponding definitions in Ebnenasir’s formalization\[[8](https://arxiv.org/html/2606.15461#bib.bib11)\], which provides the most complete publishedLDsemantics for these elements; no formal equivalence proof exists\. Ebnenasir’s formalization does not cover arithmetic function blocks \(ADD, MUL, MOVE\) and follows the sameSMT\-sort mapping as Bruttomesso et al\.\[[3](https://arxiv.org/html/2606.15461#bib.bib19)\]\. Two rules carry direct safety implications and would produce incorrect verdicts if naively implemented: \(a\) OTL/OTU latches must use set\-priority semantics – a simultaneous OTL and OTU on the same coil must leave the coil set, not cleared; \(b\) CTU edge\-triggering must detect only the rising edge of the count\-up input – a level\-sensitive CTU would double\-count events held high across scans\.

Table 6:Contact and coil element encodings to GOTO\-IRElement typeLDelementSymbolGOTO\-IRexpression/operationContactNormally\-open contact\-\-\[ v \]\-\-vNormally\-closed contact\-\-\[/v \]\-\-\!vSeries connection A–BA\-\-BA && BParallel connectionA over BA \|\| BCoilOutput\-enable coil\-\-\( q \)\-\-q = <rung\-expr\>;Set \(latch\) coil\-\-\(S q\)\-\-if \(<rung\-expr\>\) q = true;Reset \(unlatch\) coil\-\-\(R q\)\-\-if \(<rung\-expr\>\) q = false;Negated coil\-\-\(/q\)\-\-q = \!<rung\-expr\>;
#### 7\.3\.4Timer and Counter Encoding

TON timers \(see Listing[2](https://arxiv.org/html/2606.15461#LST2)\)\.The on\-delay timer is encoded as an integer state machine with a static accumulator that increments by one per scan cycle when the enable input is TRUE, and resets to zero when FALSE\. The output coil activates when the accumulator reaches the preset value\. This*fixed\-tick*model is sound forBMC: an overflow property fires when the accumulator value exceeds the preset, corresponding to a delay of exactlyPREscan cycles\.

Tick\-model note\.In ESBMC\-PLC’s verification model, timer preset values \(TON\_PRE,TOF\_PRE, etc\.\) are interpreted as a number of*scan cycles*, not as milliseconds\.IEC61131\-3TIMEliterals \(e\.g\.,T\#5s = 5000\) represent milliseconds; users must convert such values to the corresponding cycle count for their target scan period before specifying properties or instantiating timer blocks in theirLDprograms\. The conversion is exact and bounded:

PRE\_cycles=⌊TIME\_msscan\_period\_ms⌋\\texttt\{PRE\\\_cycles\}=\\left\\lfloor\\frac\{\\texttt\{TIME\\\_ms\}\}\{\\texttt\{scan\\\_period\\\_ms\}\}\\right\\rfloorFor example, a 5\-second delay \(T\#5s\) at a10ms10\\text\{\\,\}\\mathrm\{ms\}scan period corresponds toPRE\_cycles= 500\. The one\-sided rounding error is at most one scan period; for a10ms10\\text\{\\,\}\\mathrm\{ms\}scan period, the maximum timer under\-run is<<10ms10\\text\{\\,\}\\mathrm\{ms\}, which is negligible in safety analysis relative toIEC62061 safety\-function response\-time margins\.

CTU counters \(see Listing[2](https://arxiv.org/html/2606.15461#LST2)\)\.The count\-up counter uses*edge\-triggered*semantics: the accumulator increments only on a rising edge of the count\-up input, detected using a shadow Boolean variable that stores the previous\-cycle input value\. The reset input takes priority over the count\-up input\.

1

2staticuint32\_tTON\_ACC=0;

3staticboolTON\_Q=false;

4if\(TON\_IN\)\{if\(TON\_ACC<TON\_PRE\)TON\_ACC\+\+;\}

5elseTON\_ACC=0;

6TON\_Q=\(TON\_ACC\>=TON\_PRE\);

7

8

9staticuint32\_tCTU\_ACC=0;

10staticboolCTU\_CU\_PREV=false;

11if\(CTU\_CU&&\!CTU\_CU\_PREV\)

12if\(CTU\_ACC<UINT32\_MAX\)CTU\_ACC\+\+;

13CTU\_CU\_PREV=CTU\_CU;

14if\(CTU\_R\)CTU\_ACC=0;

15CTU\_Q=\(CTU\_ACC\>=CTU\_PRE\);

Listing 2:TON and CTU encodings

### 7\.4Property Specification Language

Safety properties are specified in a YAML file passed via the\-\-ld\-propsflag\. ESBMC\-PLC supports five property kinds, chosen to cover the most frequent safety requirements inICSwithout requiring automation engineers to write formal temporal logic:

Table 7:ESBMC\-PLC property kindsKindSemanticsExamplemutual\_exclusionVariablesv1,…,vnv\_\{1\},\\ldots,v\_\{n\}are never all TRUE simultaneouslyForward and reverse motorsinvariantExpression is TRUE in every scan cycleEstop implies motor offabsenceExpression is never TRUEPump and valve simultaneously onresponseWithinNNscans of trigger, response holdsStop signal acknowledged within 3 cyclesreachabilityExpression is reachable \(liveness check, inverted verdict\)Output can ever activate#### 7\.4\.1Justification Enforcement

For theresponseandreachabilityproperties, thejustificationfield is required to document the timing assumption\. This design decision is motivated by the difficulty of specifying timing constraints noted in\[[9](https://arxiv.org/html/2606.15461#bib.bib18)\], where implicit temporal assumptions inPLCsafety properties are identified as a source of specification errors\.

Listing[3](https://arxiv.org/html/2606.15461#LST3)shows a representative property file\.

1properties:

2\-id:P1

3kind:mutual\_exclusion

4variables:\[Motor\_Forward,Motor\_Reverse\]

5description:"Forwardandreversemustneverbeactivetogether"

6

7\-id:P2

8kind:invariant

9expression:"\!Emergency\_Stop\|\|\!Motor"

10description:"Emergencystopmustdisablemotor"

11

12\-id:P3

13kind:response

14trigger:"Emergency\_Stop"

15response:"\!Motor"

16max\_scans:1

17justification:"ImmediatestoprequiredbyIEC62061clause6\.7\.4"

18description:"Motorstopswithin1scanafteremergencystop"

Listing 3:Example YAML property file

### 7\.5Verification Backend and Tool Usage

ESBMC\-PLC usesESBMCwith Z3 4\.13\.0 as the defaultSMTbackend\. Two verification modes are supported:

- •IncrementalBMC\(\-\-incremental\-bmc\): explores increasing unwind depths until a counterexample is found or the bound is exhausted\. This is the recommended mode for programs expected to have violations; it finds bugs quickly without requiring a manual unwind bound\.
- •k\-induction\(\-\-k\-induction \-\-unlimited\-k\-steps\): for invariant\-class properties \(mutual\_exclusion,invariant,absence, andresponse\), proves that the property holds for all possible input sequences and all scan counts, when the induction step converges\. This provides an unbounded safety guarantee thatBMCalone cannot give and is the mode used for SAFE variants in the evaluation\.Reachabilityproperties are handled by incrementalBMCregardless of this flag; see the guarantee mapping below\.

#### 7\.5\.1Property\-kind Guarantee Mapping

mutual\_exclusion,invariant, andabsenceare state invariants and are proved unconditionally byk\-induction\. Aresponse\(trigger, expr, max\_scans=N\)property is compiled to the safety invariant “after any trigger event,exprholds within the nextNNscan cycles”;k\-induction then proves this invariant holds for all future trigger occurrences, providing an unbounded guarantee on the bounded\-horizon safety condition\. Areachabilityproperty invokes incrementalBMCto confirm the expression is reachable at some boundk≥1k\\geq 1; its guarantee is therefore bounded\.

Standard invocation:

```
# Bug-finding mode (unsafe programs):
ld-verify program.ld --ld-props props.yaml --incremental-bmc

# Unbounded proof mode (safe programs):
ld-verify program.ld --ld-props props.yaml \
  --\textit{k}-induction --unlimited-k-steps
```

Exit codes are structured forContinuous Integration and Continuous Deployment \(CI/CD\)integration:0= SAFE,10= VIOLATION \(with counterexample\),1= UNKNOWN,2= ERROR\. JSON output is available via\-\-json\.

#### 7\.5\.2Counterexample Presentation

WhenESBMCreports a violation, the counterexample trace uses the originalLDvariable names from the PLCopen XML file \(not mangledIRnames\)\. It identifies the specific scan cycle and property violated\. This makes counterexamples directly interpretable by automation engineers without knowledge of the underlyingIR\.

## 8Experimental Evaluation

To evaluate ESBMC\-PLC systematically, we first define the research questions that guide our experiments\. Following that, we describe the benchmark suite and experimental setup and then present results organized by benchmark category\. Each category progressively increases in complexity and realism: Category A contains original ESBMC\-PLC benchmarks designed to validate basic correctness; Category B comprises synthetic industrial programs derived from safety\-critical patterns in the literature; Category C introduces unmodified real\-world vendor programs to assess practical usability\. For each benchmark, we report verification outcome, runtime, induction depth, and – where violations occur – a concrete counterexample and an actionable fix\. All experiments are reproducible using the open\-source toolchain described below\.

### 8\.1Research Questions

This study is structured around five research questions \(RQs\) that address the core capabilities of ESBMC\-PLC:

RQ1Can ESBMC\-PLC correctly classify safe and unsafeLDprograms across diverse industrial domains?

RQ2Are ESBMC\-PLC’s counterexamples actionable – i\.e\., do they identify the faulty rung and admit a plain\-language fix?

RQ3Can ESBMC\-PLC provide unbounded safety proofs for verified programs viak\-induction?

RQ4Does ESBMC\-PLC scale to real\-worldPLCprograms obtained directly from vendor repositories?

RQ5How does ESBMC\-PLC’s verification performance and capability compare to the state of the art \(PLCverif\)?

### 8\.2Benchmark Suite

We evaluate ESBMC\-PLC on 13 benchmarks across three categories, totalling 61 properties verified and 6 industrial domains\. Table[8](https://arxiv.org/html/2606.15461#S8.T8)provides an overview\.

Table 8:Benchmark suite overviewIDNameOriginDomainPropsCategory A: Original ESBMC\-PLC BenchmarksCS1motor\_interlockESBMC\-PLC originalMotors3CS2conveyor\_sequencingESBMC\-PLC originalTransport3CS3emergency\_shutdownESBMC\-PLC originalSafety4Category B: Synthetic Industrial Benchmarks \(literature\-derived\)CS4traffic\_light\_unsafeLiterature\[[12](https://arxiv.org/html/2606.15461#bib.bib16),[27](https://arxiv.org/html/2606.15461#bib.bib3)\]Infrastructure8CS5traffic\_light\_safeLiteratureInfrastructure8CS6bottle\_filling\_unsafeLiteratureFood industry5CS7bottle\_filling\_safeLiteratureFood industry5CS8elevator\_unsafeLiteratureBuildings6CS9elevator\_safeLiteratureBuildings6Category C: Real\-World Vendor ProgramsCS10water\_controlCONTROLLINO\[[4](https://arxiv.org/html/2606.15461#bib.bib25)\]\(MIT\)Water control4CS11stairs\_lightCONTROLLINO\[[4](https://arxiv.org/html/2606.15461#bib.bib25)\]\(MIT\)Building auto\.3CS12tank\_level\_unsafeMathWorks\[[19](https://arxiv.org/html/2606.15461#bib.bib26)\]\(public\)Process control4CS13tank\_level\_safeMathWorks\[[19](https://arxiv.org/html/2606.15461#bib.bib26)\]\(public\)Process control3Total6 domains61
### 8\.3Experimental Setup

We evaluated ESBMC\-PLC using the hardware and software configuration detailed in Table[9](https://arxiv.org/html/2606.15461#S8.T9)\. All benchmarks were executed with a 300\-second timeout, and each experiment was repeated three times to report median values\.

Table 9:Hardware and software configurationComponentSpecificationCPUApple M\-series \(ARM64 aarch64, 8 cores\)RAM16 GBOSmacOS 26 \(Tahoe\)ESBMCv7\.6\.0 \(build:ENABLE\_LD\_FRONTEND=On,RelWithDebInfo\)SMTsolverZ3 4\.13\.0CompilerClang 18 \(LLVM 18, Apple Silicon\)Timeout300s300\\text\{\\,\}\\mathrm\{s\}per runRepetitions3 runs \(median reported\)
### 8\.4Category A: Original ESBMC\-PLC Benchmarks

#### 8\.4\.1CS1 – Motor Interlock \(Safe\)

A basic motor run\-permit circuit: the motor starts onI\_Start, latches viaQ\_Motor, and must stop immediately onI\_EStop\(normally\-closed contact in series\)\. Three properties are verified: \(P1\)mutual\_exclusionon\{I\_EStop, Q\_Motor\}, \(P2\)invariant\!I\_EStop \|\| \!Q\_Motor, \(P3\)responsewithmax\_scans=1\. ESBMC\-PLC proves all three properties viak\-induction \(k=2\) in 0\.05 s, providing an unconditional safety guarantee for all input sequences and scan counts\.

#### 8\.4\.2CS2 – Conveyor Sequencing \(Violation Found\)

A five\-rung conveyor control program\.Bug found:the emergency stop signal correctly deactivates the conveyor motor in Rung 3, but does not reset the TON timer enabling Rung 5 \(the indexing step\)\. WhenI\_EStopis released, the indexing step activates immediately because the timer had already accumulated to its preset – bypassing the required re\-sequencing interlock\.

Property violated:P2 –invariant\!Emergency\_Stop \|\| \!Timer\_Step\_Active\.

Counterexample \(cycle 1\):I\_EStop=TRUE, TON\_ACC=PRE, Timer\_Step\_Active=TRUE→\\rightarrowP2 violated\.

Fix:Add\[/ Emergency\_Stop\]normally\-closed contact to the TON enable rung, resetting the timer whenever the emergency stop is active\. ESBMC\-PLC confirmed the fix by verifying the corrected program\.

#### 8\.4\.3CS3 – Emergency Shutdown \(Violation Found\)

A four\-rung emergency shutdown circuit\.Bug found:the reset logic \(Rung 4\) uses an OTL latch that overrides the emergency shutdown signal whenI\_ResetandI\_ESDare simultaneously TRUE – a sensor fault condition that physical testing may never encounter\.

Property violated:P3 –absenceI\_ESD && Q\_Pump && Q\_Valve\.

Fix:Add\[/ I\_ESD\]contact to the reset rung, preventing the reset from overriding an active emergency shutdown\.

### 8\.5Category B: Synthetic Industrial Benchmarks

Synthetic benchmarks CS4–CS9 are paired with unsafe/safe variants modeling three industrial domains: traffic light control \(infrastructure\), bottle\-filling line \(food industry\), and elevator control \(buildings\)\. Each unsafe variant contains a deliberate safety defect; each safe variant contains the corrected logic\. All were created by the authors from patterns documented in thePLCsafety literature\[[12](https://arxiv.org/html/2606.15461#bib.bib16),[27](https://arxiv.org/html/2606.15461#bib.bib3),[8](https://arxiv.org/html/2606.15461#bib.bib11)\]\.

#### 8\.5\.1CS4/CS5 – Traffic Light Control

A 21\-rung traffic light controller managing four phases \(NS\_Green, EW\_Green, NS\_Yellow, EW\_Yellow\) and pedestrian signals\. Eight properties enforce phase mutual exclusion and pedestrian\-signal consistency\.

CS4 \(Unsafe\) – Bug 1:No structural interlocks between phase timer rungs\. All four TON timers can fire simultaneously in the same nondeterministic scan when all inputs are set, makingNS\_Green=EW\_Green=1reachable\.Fix:Add negated contact for each conflicting phase to every phase\-activation rung\.

CS4 \(Unsafe\) – Bug 2 \(found during safe\-variant development\):Emergency\_VehiclesuppressesNS\_Greenin Rung 13, but Rung 19 still activatesPed\_NS\_Walkwithout checkingEmergency\_Vehicle– pedestrians receive a walk signal with no corresponding green lamp\.Fix:Add\[/ Emergency\_Vehicle\]contact to the pedestrian walk rung\.

CS5 \(Safe\):proved byk\-induction \(k=2, 0\.04 s\) after both fixes are applied\.

#### 8\.5\.2CS6/CS7 – Bottle Filling Line

An eight\-rung bottle filling and conveyor system\.Bug \(CS6\):the conveyor motor rung activates whenFilling\_Done && Conveyor\_Readywithout checkingEmergency\_Stop\. Property P5 \(absenceEmergency\_Stop && Conveyor\_Motor\) is violated in cycle 1\.Fix:Add\[/ Emergency\_Stop\]contact to the conveyor motor activation rung\.

#### 8\.5\.3CS8/CS9 – Elevator Control

A twelve\-rung elevator control program\.Bug 1 \(CS8\):Motor\_Up and Motor\_Down rungs do not checkEmergency\_Stopor the overload sensor\. Property P2 \(absenceEmergency\_Stop && Motor\_Up\) violated in cycle 1\.

Bug 2 \(discovered during fix verification\):a one\-scan race condition –Motor\_Up=1in scanNN, butMotor\_Running=0because Rungs 10–11 have not yet executed in the same scan, causingDoor\_Opento activate in the same scan as motor start\.Fix:Door\_Openrung checksMotor\_UpandMotor\_Downdirectly rather thanMotor\_Running, eliminating the one\-scan lag\.

This finding illustrates a class of*scan\-cycle race conditions*that functional testing cannot detect because they require simultaneous exploration of rung execution order and input nondeterminism – precisely the scenario that ESBMC\-PLC’s nondeterministic input model covers\.

### 8\.6Category C: Real\-World Vendor Programs

To evaluate ESBMC\-PLC on programs not designed for verification purposes, we selected two programs from the CONTROLLINO\-PLC open\-sourcePLCexamples repository\[[4](https://arxiv.org/html/2606.15461#bib.bib25)\]\(MIT License, hardware: CONTROLLINO MAXI Automation, programs created 2024\-11\-13\) and two variants of the MathWorks SimulinkPLCCoder tank\-level example\[[19](https://arxiv.org/html/2606.15461#bib.bib26)\]\.

CS10 – Water Reserve Control\.Source:water\_control/plc\.xmlfrom the CONTROLLINO repository\. The program controls a water pump based on pool and tank level sensors\. Variables:Pool\_Low\_Level\_Sensor\(%IX0\.0\),Tank\_High\_Level\_Sensor\(%IX0\.1\),Tank\_Low\_Level\_Sensor\(%IX0\.2\),Automatic\_Manual\_Switch\(%IX0\.3\),Stop\_Button\(%IX0\.4\),Start\_Button\(%IX0\.5\),Water\_Pump\(%QX0\.0\)\. The file was copied*without modification*from the repository directly to ESBMC\-PLC’s benchmark directory\. ESBMC\-PLC parsed the graphical PLCopen XML format with coordinate\-based connections without any manual editing, proving 4 properties viak\-induction \(k=2\) in 0\.03 s\.

CS11 – Staircase Light Control\.Source:stairs\_light\_control/plc\.xml, CONTROLLINO repository\. A PIR\-triggered staircase light with a TOF off\-delay timer and two manual override buttons\. Proved 3 properties in 0\.03 s\.

CS12/CS13 – Tank Level Control\.Derived from the MathWorks SimulinkPLCCoder documentation example\[[19](https://arxiv.org/html/2606.15461#bib.bib26)\]: a pump fills the tank whenLOW\_SWITCH=1; a valve drains it whenHIGH\_SWITCH=1\.CS12 \(Unsafe\) – Bug found:No interlock betweenPUMPandVALVE\. WhenHIGH\_SWITCH=1andLOW\_SWITCH=1simultaneously \(a physically plausible sensor\-fault condition\), both pump and valve activate, causing property P1 \(absencePUMP && VALVE\) to be violated\.Fix \(CS13\):Added\[/ HIGH\_SWITCH\]to the pump rung and\[/ LOW\_SWITCH\]to the valve rung, plusDraining\_Active/Filling\_Activeinterlocks; all 3 safe properties proved in 0\.03 s\.

This real\-world bug illustrates ESBMC\-PLC’s ability to detect*sensor fault scenarios*: the nondeterministic input model enables ESBMC\-PLC to explore electrically plausible yet physically unlikely sensor states, thereby revealing design assumptions that should be made explicit via interlocks\.

### 8\.7Results Summary

Table[10](https://arxiv.org/html/2606.15461#S8.T10)presents verification results for all 13 programs\.

Table 10:Verification results\. ✓ = correct classificationIDProgramExp\.ResultCorr\.Time \(s\)kPropsCS1motor\_interlockSAFESAFE✓\\checkmark0\.0523CS2conveyor\_sequencingVIOLATIONVIOLATION✓\\checkmark0\.0413CS3emergency\_shutdownVIOLATIONVIOLATION✓\\checkmark0\.0414CS4traffic\_light\_unsafeVIOLATIONVIOLATION✓\\checkmark0\.0318CS5traffic\_light\_safeSAFESAFE✓\\checkmark0\.0428CS6bottle\_filling\_unsafeVIOLATIONVIOLATION✓\\checkmark0\.0315CS7bottle\_filling\_safeSAFESAFE✓\\checkmark0\.0525CS8elevator\_unsafeVIOLATIONVIOLATION✓\\checkmark0\.0316CS9elevator\_safeSAFESAFE✓\\checkmark0\.0526CS10water\_controlSAFESAFE✓\\checkmark0\.0324CS11stairs\_lightSAFESAFE✓\\checkmark0\.0323CS12tank\_level\_unsafeVIOLATIONVIOLATION✓\\checkmark0\.0314CS13tank\_level\_safeSAFESAFE✓\\checkmark0\.0323Correct classification13/13max: 0\.0561False positives / False negatives0 / 0
### 8\.8Bugs Found

Table[11](https://arxiv.org/html/2606.15461#S8.T11)summarises the eight bugs found by ESBMC\-PLC across the benchmark suite\. Six were found in the initial evaluation runs \(one primary bug per unsafe program\); two additional defects \(CS4†and CS8†\) were discovered by ESBMC\-PLC during fix\-verification re\-runs\.

Table 11:Bugs found by ESBMC\-PLC, with responsible rung and fixIDBug descriptionProperty violatedFixCS2E\-stop does not reset TON timer\!EStop \|\| \!Timer\_ActiveAdd\[/EStop\]to TON enable rungCS3Reset overrides ESD signal\!ESD \|\| \!Pump \|\| \!ValveAdd\[/ESD\]to reset rungCS4No phase interlocks; simultaneous phases\!\(NS\_Green && EW\_Green\)Add negated contacts for each conflicting phaseCS4†Emergency vehicle not propagated to pedestrian walk rung\!Emerg\_Vehicle \|\| \!Ped\_NS\_WalkAdd\[/Emergency\_Vehicle\]to pedestrian walk rungCS6E\-stop not propagated to conveyor\!EStop \|\| \!ConveyorAdd\[/EStop\]to conveyor rungCS8Motor runs during emergency\!EStop \|\| \!Motor\_UpAdd\[/EStop\],\[/Overload\]to motor rungsCS8†One\-scan lag:Door\_Openactivates on same scan as motor start\!\(Motor\_Up && Door\_Open\)CheckMotor\_Up/Motor\_Downdirectly in door rungCS12PUMP and VALVE simultaneously active\!\(PUMP && VALVE\)Add\[/HIGH\_SW\]to pump;\[/LOW\_SW\]to valve†Found by ESBMC\-PLC during fix\-verification re\-run, not the initial evaluation pass\.
### 8\.9Translation Conformance Validation

#### 8\.9\.1Translation Soundness

To empirically validate the correctness of theLD→\\toGOTO\-IRtranslation, we extracted thescan\_looplogic from the GOTOIRof each benchmark using the\-\-goto\-functions\-onlyflag and re\-executed it as a concrete reference interpreter over 2,000 input combinations \(50 sequences×\\times10 scans per benchmark, random seed 42\)\. We verified three properties of the generated GOTOIR: \(i\) input variables are re\-sampled viaNONDET\(\_Bool\)at every scan boundary, faithfully modelling theIEC61131\-3cyclic execution semantics; \(ii\) the rung assignments in thescan\_loopfaithfully reflect the PLCopen XML source, including correct handling of parallel rungs \(multiple coil\-driving rungs are OR\-combined\) and TON timer semantics \(elapsed\-time counter incremented per scan, output latched whenET≥PT\\texttt\{ET\}\\geq\\texttt\{PT\}\); \(iii\) all safety properties hold across all 2,000 concrete executions with zero divergences \(Table[12](https://arxiv.org/html/2606.15461#S8.T12)\)\.

Two benchmarks \(water\_control,stairs\_light\) use the graphical PLCopen XML format \(tc6\_0201\) with coordinate\-based connections \(refLocalId/localId\)\. The ESBMC\-PLC parser accepts these files without modification\. Still, the currentLD→\\toGOTO\-IRconverter does not yet emit rung logic for graphical connections – a known limitation documented in Section[11](https://arxiv.org/html/2606.15461#S11)\. These two benchmarks are excluded from Table[12](https://arxiv.org/html/2606.15461#S8.T12)and counted as a known gap rather than a verified result\.

#### 8\.9\.2Methodology

For each benchmark with complete GOTO\-IR\(textualLDformat\), we extracted thescan\_loopvia\-\-goto\-functions\-only, re\-executed it as a Python reference interpreter over 50 randomly generated input sequences \(seed 42, each of 10 scan cycles\), and checked all safety properties on every output state\. The random input generator respects physical constraints \(e\.g\.,HIGH\_SWITCHandLOW\_SWITCHare never simultaneously true for the tank benchmark\)\. All 2,000 scans passed all properties, providing empirical evidence that theLD→\\toGOTO\-IRtranslation preserves the safety semantics of the originalLDprograms\.

Table 12:Concrete GOTO\-IRexecution vs\. safety properties\. Inputs: 50 random sequences×\\times10 scans \(seed 42\)\. Divergence = scan output violates the propertyBenchmarkScansDivergencesStatustraffic\_light\_safe5000✓\\checkmarkbottle\_filling\_safe5000✓\\checkmarkelevator\_safe5000✓\\checkmarktank\_level\_safe5000✓\\checkmarkwater\_controlN/Agraphicaltc6\_0201†stairs\_lightN/Agraphicaltc6\_0201†Total2,0000All pass
†Parser accepts the file; rung\-logic conversion for graphical connections not yet implemented \(see Section[11](https://arxiv.org/html/2606.15461#S11)\)\.

#### 8\.9\.3Notable Findings

Two bug patterns appeared repeatedly across independent benchmarks: \(1\)*emergency/override propagation failure*– an emergency or override signal correctly suppresses the primary actuator but is not propagated to all dependent outputs \(CS2, CS3, CS4†, CS6\) – and \(2\)*missing interlocks under sensor fault conditions*– the design assumes sensors are physically mutually exclusive but does not enforce this electrically \(CS8, CS12\)\. Both patterns are well\-known inPLCsafety engineering\[[23](https://arxiv.org/html/2606.15461#bib.bib4)\]but are not detectable by conventional functional testing\.

## 9Comparison with PLCverif

PLCverif\[[17](https://arxiv.org/html/2606.15461#bib.bib7),[16](https://arxiv.org/html/2606.15461#bib.bib20)\]is the most mature open\-source formal verification platform forPLCprograms, developed atCERNand in production use since 2019\. This section provides a systematic comparison of features\.Direct runtime comparison is not possiblebecause PLCverif does not supportLDinput: it requires SiemensSCL\(aSTdialect\), and noLD\-to\-SCLconversion preserving semantic fidelity is available\. The comparison is therefore based on published documentation\[[17](https://arxiv.org/html/2606.15461#bib.bib7),[16](https://arxiv.org/html/2606.15461#bib.bib20)\]and the PLCverif open\-source repository\.

Unlike PLCverif, which relies on theCBMCbackend and does not supportk\-induction\[[17](https://arxiv.org/html/2606.15461#bib.bib7)\], ESBMC\-PLC usesESBMCwith Z3 and provides unbounded safety proofs viak\-induction\.The PLCverif authors themselves identifiedESBMCas a direction for improvement, noting that“anSMT\-based model checker likeESBMCcould improve the performance ofCBMC”\[[17](https://arxiv.org/html/2606.15461#bib.bib7)\]; ESBMC\-PLC is a direct realisation of that planned direction forLDprograms\.

### 9\.1Input Language Support

Table[13](https://arxiv.org/html/2606.15461#S9.T13)compares the input language capabilities of ESBMC\-PLC and PLCverif\.

Table 13:Input language comparisonDimensionESBMC\-PLCPLCverifLD\(PLCopen XML\)Yes \(native\)NoST/SCL\(Siemens\)NoYesStatement List \(STL\)\(Siemens\)NoYesFBDNoVia OpennessScripterLD→\\toSTconversion required?Not neededYes \(manual or tool\-assisted\)ESBMC\-PLC is the*only*open\-source formal verifier that accepts standard PLCopen XMLLDfiles\. PLCverif requires the user to either write the program inSCLor manually translate theLDprogram, which can introduce fidelity loss and entail significant manual effort for large programs\.

### 9\.2Verification Capabilities

Table[14](https://arxiv.org/html/2606.15461#S9.T14)compares the verification capabilities of ESBMC\-PLC and PLCverif across several dimensions\.

Table 14:Verification capability comparisonDimensionESBMC\-PLCPLCverifBMCYes\(incremental\)Yes \(CBMC, bounded\)k\-induction \(unbounded proof\)YesNoSMTencoding \(bit\-vector\)Yes\(Z3\)No \(SAT\-basedCBMC\)Unbounded proof \(other\)Viak\-inductionBinary Decision Diagrams \(BDD\)\(nuXmv, limited scalability\)CEGAR abstractionNoYes \(in development\)LTL/CTLpropertiesNoYes \(via nuXmv\)Spurious counterexamplesNo\(BMC: genuine\)Possible \(\-\-partial\-loops\)The key capability advantage of ESBMC\-PLC over PLCverif isk\-induction: PLCverif provides bounded safety proofs \(up to a fixed number of steps\) orBDD\-based unbounded proofs via nuXmv, which scale poorly to programs with large integer variables\. ESBMC\-PLC proves properties for all scan counts viak\-induction withSMTencoding, providing stronger guarantees at comparable or better runtime\.

PLCverif’s advantage isfullLTL/CTL: for properties requiring temporal operators beyond the five ESBMC\-PLC property kinds, PLCverif with nuXmv remains the better choice\.

### 9\.3Property Specification

A key advantage of ESBMC\-PLC is its YAML\-based property specification, which offers a shorter learning curve than PLCverif\. Table[15](https://arxiv.org/html/2606.15461#S9.T15)compares the two approaches\.

Table 15:Property language comparisonDimensionESBMC\-PLCPLCverifFormatYAML \(\-\-ld\-props\)Inline assertions or pattern sentencesMutual exclusionYesVia patternInvariantYesVia//\# ASSERTAbsenceYesVia patternBounded responseYes \(withjustification\)Via patternReachabilityYes \(inverted verdict\)Via patternFullLTL/CTLNoYes \(nuXmv back\-end\)Learning curveLow\(YAML, no logic\)Medium \(patterns\) to High \(LTL/CTL\)
### 9\.4IEC61131\-3Construct Coverage

Table[16](https://arxiv.org/html/2606.15461#S9.T16)shows the coverage ofIEC61131\-3constructs in ESBMC\-PLC compared to PLCverif\.

Table 16:IEC61131\-3construct supportConstructESBMC\-PLCPLCverifBOOL contacts/coils \(XIC/XIO/OTE\)YesYes \(viaST\)Latching coils \(OTL/OTU\)YesYesTON/TOF/TP timersYesYesCTU/CTD countersYesYesArithmetic FBs \(ADD, MUL, MOVE\)YesYesBOOL/INT/DINT/TIME typesYesYesREAL/FLOAT typesNoYesSTRING typesNoYesArraysNoPartial \(recent\)Multiple POUs/function callsNoYesInterrupt tasksNoYesESBMC\-PLC currently covers the constructs found in the vast majority of safety\-criticalLDprograms \(Boolean logic, timers, counters, integer arithmetic\)\. REAL/FLOAT types, strings, arrays, and multi\-POU programs are planned for future releases\.

### 9\.5Performance

Table[17](https://arxiv.org/html/2606.15461#S9.T17)shows that ESBMC\-PLC verifiesLDbenchmarks efficiently, typically within sub\-second times, while PLCverif does not natively supportLD\.

Table 17:Performance comparison on available benchmarksBenchmarkESBMC\-PLCPLCverif \(reported\)motor\_interlock \(2 rungs, 3 props\)0\.05 s\(k\-ind\., proved\)Not reported \(noLDsupport\)conveyor\_sequencing \(5 rungs, 3 props\)0\.04 s\(violation, k=1\)Not applicabletraffic\_light\_safe \(21 rungs, 8 props\)0\.04 s\(k\-ind\., proved\)Not applicableCERNSPS\-PPS \(largeSTprogram\)Not applicable \(noSTsupport\)Several minutes \(nuXmvBDD\)\[[16](https://arxiv.org/html/2606.15461#bib.bib20)\]The input language gap precludes direct timing comparison\. TheCERNSPS\-PPS benchmark, verifiable with PLCverif, is a largeSCLprogram with no PLCopen XML counterpart\. ESBMC\-PLC’s sub\-60ms60\\text\{\\,\}\\mathrm\{ms\}results for all 13 benchmarks are consistent with prior results showingESBMCmatches or outperforms NuSMV onPLC\-sized programs\[[22](https://arxiv.org/html/2606.15461#bib.bib8)\]\.

### 9\.6Summary Assessment

Table[18](https://arxiv.org/html/2606.15461#S9.T18)summarizes the key differences between ESBMC\-PLC and PLCverif\. ESBMC\-PLC excels at unbounded verification ofLDprograms with a simple property language, while PLCverif is a mature tool for Siemens text\-based languages\.

Table 18:Overall comparison summaryCategoryESBMC\-PLCPLCverifBest forLDprograms \(PLCopen XML\)SiemensST/STLprogramsProof strengthUnbounded\(k\-induction\)Bounded \(CBMC\) orBDD\(nuXmv\)Property languageSimple YAML \(5 kinds\)Patterns orLTL/CTLNativeLDsupportYesNoSMTbit\-vector encodingYesNoMaturityPrototype \(2026\)Production \(CERN, 2019\+\)LicenceMIT \(viaESBMC\)EPL\-2\.0ESBMC\-PLC and PLCverif are complementary tools: ESBMC\-PLC is the right choice for any program authored in or exportable to PLCopen XMLLDformat, while PLCverif is the right choice for SiemensSCL/STLprograms or properties requiring full temporal logic\. Integrating ESBMC\-PLC’sLDfrontend into PLCverif \(and substitutingESBMCforCBMC, as the PLCverif authors suggested\) would produce a unified platform for both languages – this is the primary future direction discussed in Section[12](https://arxiv.org/html/2606.15461#S12)\.

## 10Discussion

RQ1 – Correct classification\.ESBMC\-PLC correctly classifies all 13 benchmarks \(7 safe, 6 unsafe\) across 6 industrial domains with zero false positives and zero false negatives\.Provenance note:Categories A and B \(CS1–CS9\) are author\-constructed with safe/unsafe labeling assigned by design; correct classification over these confirms that the inserted fault patterns are detectable, not a claim of generalization\. The strongest independent validation is Category C \(CS10–CS13, §[8\.6](https://arxiv.org/html/2606.15461#S8.SS6)\), which uses programs obtained from vendor repositories and not designed for verification purposes; correct classification there reflects the fidelity of theLD\-to\-GOTO\-IRtranslation on programs unseen during tool development\. These results are consistent with prior evaluations ofESBMConPLCprograms\[[25](https://arxiv.org/html/2606.15461#bib.bib9),[22](https://arxiv.org/html/2606.15461#bib.bib8)\]\.

RQ2 – Actionable counterexamples\.In all six unsafe programs, ESBMC\-PLC’s counterexample trace identifies the specific scan cycle, the violated property, and the originalLDvariable names responsible for the violation\. Each counterexample admits a plain\-language fix \(Table[11](https://arxiv.org/html/2606.15461#S8.T11)\) that was verified by rerunning ESBMC\-PLC on the corrected program\. Two bug patterns – emergency\-propagation failure and missing sensor\-fault interlocks – appeared independently in multiple benchmarks across different domains, suggesting they represent systematicLDdesign anti\-patterns not detectable by conventional simulation\.

RQ3 – Unbounded proofs viak\-induction\.For all 7 safe programs,k\-induction provides unconditional safety proofs \(k=2 in all cases\) in under60ms60\\text\{\\,\}\\mathrm\{ms\}\. This demonstrates that ESBMC\-PLC’sSMT\-basedk\-induction is practically efficient for the class of programs evaluated and produces stronger guarantees than bounded model checking alone\. The uniform convergence at k=2 reflects the benchmark complexity: all safe programs have safety invariants with a one\-cycle inductive step\. Real industrial programs with deep counter\-dependent state or multi\-timer coordination may require largerkk; evaluation on larger external benchmarks \(§[11](https://arxiv.org/html/2606.15461#S11)\) will establish the practical range ofkkfor this tool\.

RQ4 – Real\-world vendor programs\.ESBMC\-PLC successfully parsed and verified PLCopen XML files exported directly from the CONTROLLINO toolchain without any modification, demonstrating that the parser correctly handles the graphicaltc6\_0201format used by deployed industrialPLCs\. The tank\-level bug found in the MathWorks example \(simultaneous PUMP and VALVE activation under sensor fault\) is a realistic design error that would not be exposed by standard simulation testing, which typically assumes sensors are never simultaneously active in a physically impossible state\.

RQ5 – Comparison with PLCverif\.ESBMC\-PLC provides three capabilities not available in PLCverif: \(i\) nativeLDinput \(no translation required\), \(ii\) unbounded safety proofs viak\-induction, and \(iii\)SMTbit\-vector arithmetic \(enabling overflow detection\)\. PLCverif retains advantages in fullLTL/CTLproperty support,ST/SCLinput, and production maturity\. The tools address complementary use cases, and a unified platform integrating both is the logical next step\.

Performance\.All 13 runs complete in under60ms60\\text\{\\,\}\\mathrm\{ms\}on Apple Silicon \(aarch64\), comfortably below the 300\-second timeout and practical forCI/CDsintegration in industrial development workflows\. TheSMT\-based approach does not require manual unwind bounds – incrementalBMCfinds violations as quickly as possible, andk\-induction terminates as soon as the inductive invariant is strong enough\.

Limitations\.\(1\) ESBMC\-PLC’s translation rules are not yet formally proved equivalent to theIEC61131\-3standard; correctness is established empirically via the benchmark results and consistency with Ebnenasir’s semantics\[[8](https://arxiv.org/html/2606.15461#bib.bib11)\]\. \(2\) REAL/FLOAT types, arrays, strings, and multi\-POU programs are not yet supported; programs using these constructs generate anUnsupportedConstructerror\. \(3\) The benchmark suite, while covering three sources and six domains, is still small relative to the diversity of deployedPLCprograms; evaluation on the PLCOpen benchmark suite\[[24](https://arxiv.org/html/2606.15461#bib.bib10)\]and SWaTLDdataset\[[12](https://arxiv.org/html/2606.15461#bib.bib16)\]is needed to establish broader coverage\.

## 11Threats to Validity

Internal validity\.All benchmarks in Categories A and B were created by the authors; safe/unsafe labeling is ground truth by design\. Results could differ on independently collected programs with more complex rung dependencies or vendor\-specific extensions\. The fix proposals in Table[11](https://arxiv.org/html/2606.15461#S8.T11)were each verified by rerunning ESBMC\-PLC on the corrected program, confirming that the fixes address the reported violations\.

External validity\.Thirteen programs in six domains provide broader coverage than most prior evaluations in the period under review\[[2](https://arxiv.org/html/2606.15461#bib.bib5),[12](https://arxiv.org/html/2606.15461#bib.bib16)\]\. Still, they are not a representative sample of the full space of deployed industrialPLCprograms\. The PLCOpen benchmark suite\[[24](https://arxiv.org/html/2606.15461#bib.bib10)\]\(40 programs, all fromST\) and the SWaTLDdataset\[[12](https://arxiv.org/html/2606.15461#bib.bib16)\]\(60 programs\) are the appropriate next evaluation targets\. Category C programs \(CONTROLLINO, MathWorks\) significantly strengthen external validity by involving programs not designed for verification purposes\.

Construct validity\.TheLD\-to\-GOTO\-IRencoding rules \(Table[6](https://arxiv.org/html/2606.15461#S7.T6), Listing[2](https://arxiv.org/html/2606.15461#LST2)\) are*designed*to match Ebnenasir’s formal semantics\[[8](https://arxiv.org/html/2606.15461#bib.bib11)\]for the elements it covers \(XIC/XIO, OTE/OTL/OTU, TON/TOF/TP, CTU/CTD\) but have not been formally proved equivalent to theIEC61131\-3standard\. The conformance testing of §[8\.9](https://arxiv.org/html/2606.15461#S8.SS9)\(2,000 concrete trace points across 4 safe textual\-format benchmarks\) provides empirical evidence of translation fidelity with zero divergences \(Table[12](https://arxiv.org/html/2606.15461#S8.T12)\)\. Vendor\-specificLDextensions \(e\.g\., SiemensMOVE\_BLK, RockwellMSGblocks\) are not covered\. The YAML property language covers five property kinds; programs requiring full temporal logic \(LTL/CTL\) may need PLCverif with nuXmv\.

### 11\.1GraphicalLDFormat Coverage

The ESBMC\-PLC parser accepts both the textual PLCopen XML format \(used in benchmarks CS1–CS9 and CS12–CS13\) and the graphicaltc6\_0201format produced by OpenPLC Editor v3 and Beremiz \(used in real\-vendor benchmarks CS10–CS11\)\. However, theLD→\\toGOTO\-IRconverter currently generates rung logic only for textualLD; for graphicalLD, it parses variable declarations and properties but does not yet emit the rung assignment instructions\. As a result, the GOTOIRforwater\_controlandstairs\_lightcontains only property assertions over zero\-initialized variables, making the verification trivially safe rather than genuinely sound\. We document this as a known gap and exclude these benchmarks from the conformance table \(Table[12](https://arxiv.org/html/2606.15461#S8.T12)\)\. Completing the graphical\-to\-IRconverter is planned for the immediate future\.

Measurement validity\.Timing results are the median of three runs on Apple M\-series hardware; results on other hardware will differ in absolute values, but relative differences are expected to be small for programs of this size\. All runs completed well within the 300\-second timeout, so the timeout effect does not confound the classification results\.

## 12Future Directions

Formal equivalence proof via K\-LDsemantics\.DefiningLDsemantics in the K framework – extending K\-ST\[[26](https://arxiv.org/html/2606.15461#bib.bib13)\]– would provide a reference interpreter, a compiler test oracle, and a pathway to a formally provedLD\-to\-GOTO\-IRtranslation\. This would closeGap 4and elevate ESBMC\-PLC’s soundness guarantees from empirical to provable\.

Integration with PLCVerif asLDfrontend andESBMCback\-end\.Adding ESBMC\-PLC’sLDfront\-end to PLCverif \(parsing Siemens LAD or CODESYSLD\) and substitutingESBMCfor theCBMCback\-end would leverage PLCverif’sCERN\-validatedSTpipeline while extending coverage toLDand enablingk\-induction\. The PLCverif authors identifiedESBMCas a direction for improvement\[[17](https://arxiv.org/html/2606.15461#bib.bib7)\]; ESBMC\-PLC is the realization of that direction forLDprograms\.

LLBdetection as a security application\.The security application of\[[12](https://arxiv.org/html/2606.15461#bib.bib16),[3](https://arxiv.org/html/2606.15461#bib.bib19)\]provides a high\-impact use case with clear property structure:LLBmanifest as reachability properties that map directly to ESBMC\-PLC’sabsenceproperty kind\. AnESBMC\-basedLLBdetector forLDwould combine formal rigor with industrial relevance and could be evaluated on the SWaTLDdataset\.

ExtendedIEC61131\-3coverage\.REAL/FLOAT types, arrays, and multi\-POU programs are the primary coverage gaps\. REAL types requireESBMC’s floating\-pointSMTbackend \(already supported for C programs\); arrays require a symbolic index encoding; multi\-POU support requires cross\-rung dependency analysis\.

Multitask and networked extensions\.Lee and Bae \[[13](https://arxiv.org/html/2606.15461#bib.bib15),[14](https://arxiv.org/html/2606.15461#bib.bib21)\]demonstrate that multitask preemption and networkedPLCcommunication introduce verification complexity far beyond the single\-task model\. Partial order reduction and compositional verification are the most promising directions for scaling ESBMC\-PLC to realistic multitask industrial deployments\.

LLM\-assisted translation verification\.ESBMC’s integration withLarge Language Models \(LLMs\)\[[7](https://arxiv.org/html/2606.15461#bib.bib22)\]could assistLD\-to\-GOTO\-IRtranslation: given anLDrung, an LLM generates a candidate translation, which K\-LDformally validates\. This could accelerate coverage of vendor\-specific extensions\.

## 13Conclusion

This paper presented ESBMC\-PLC, the first open\-source formal verifier with native support forIEC61131\-3LDprograms in standard PLCopen XML format\. ESBMC\-PLC is implemented as a new frontend for theESBMCmodel checker, translatingLDrungs toESBMC’s GOTO intermediate representation and encoding thePLCscan cycle as awhile\(true\)loop with nondeterministic inputs\. Users specify safety requirements in a five\-kind YAML property language without requiring expertise in temporal logic; ESBMC\-PLC checks properties viaSMT\-based bounded model checking ork\-induction for unbounded proofs\.

A systematic survey of 22 studies \(2020–2026\) identified four technical directions inPLCLDverification and four research gaps\. ESBMC\-PLC directly closes two of these gaps – the absence of an open\-sourceLD\-to\-formal\-language translator and the absence of anESBMCfrontend forIEC61131\-3– and mitigates the other two\.

The experimental evaluation on 13 benchmarks spanning six industrial domains and three program sources \(original, synthetic, real vendor programs\) demonstrated:correct classification of all 13 benchmarks– all 9 author\-constructed programs \(Categories A and B\) classified as expected by design, and all 4 independent vendor programs \(Category C\) correctly classified without pre\-assigned labels – with zero false positives;8 bugsfound with actionable counterexamples identifying the responsible rung;7 unbounded safety proofsviak\-induction; andall 61 property checkscompleting in under60​ms60\\,\\text\{ms\}on Apple Silicon \(aarch64\)\. Real\-world vendor programs \(CONTROLLINO, MathWorks\) were parsed and verified directly from their exported PLCopen XML files without any preprocessing\.

The comparison with PLCverif – the state\-of\-the\-artPLCformal verification platform – shows that ESBMC\-PLC is the only open\-source tool providing nativeLDinput,k\-induction unbounded proofs, andSMTbit\-vector arithmetic together\. At the same time, PLCverif retains advantages forST/SCLprograms that require full temporal logic\. These tools are complementary; a unified platform integrating ESBMC\-PLC’sLDfrontend with PLCverif’sSTpipeline andESBMCas the common backend is the primary direction for future work\.

The central findingis that, for the class of programs evaluated, the formal verification of industrialPLCLadder Logic programs is a practical, open\-source, sub\-second operation available to any automation engineer with a PLCopen XML export from their development environment\. Broader generalization – to larger programs, a wider benchmark corpus, and a formally proved translation layer – remains the path to industrial\-scale deployment\.

### Artefact Availability

The complete artifact – including all 13 benchmarks, property files, the conformance testing package, and the ESBMC\-PLC binary – is permanently archived at Zenodo\[[6](https://arxiv.org/html/2606.15461#bib.bib23)\]\([https://doi\.org/10\.5281/zenodo\.20680071](https://doi.org/10.5281/zenodo.20680071)\)\. The conformance experiments \(Table[12](https://arxiv.org/html/2606.15461#S8.T12)\) can be reproduced with a single command:bash conformance/run\_all\.sh

### Acknowledgments

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, and EP/X037290/1, and from the Soteria project, awarded by UK Research and Innovation under the Digital Security by Design \(DSbD\) Program\.

## References

- \[1\]\(2021\)Automated verification of temporal properties of ladder programs\.InFormal Methods for Industrial Critical Systems \(FMICS 2021\),Lecture Notes in Computer Science\.External Links:[Document](https://dx.doi.org/10.1007/978-3-030-85248-1%5F2),[Link](https://link.springer.com/chapter/10.1007/978-3-030-85248-1_2)Cited by:[§2\.4](https://arxiv.org/html/2606.15461#S2.SS4.p1.1),[§3\.4](https://arxiv.org/html/2606.15461#S3.SS4.p1.1),[§4\.2](https://arxiv.org/html/2606.15461#S4.SS2.p2.1),[Table 2](https://arxiv.org/html/2606.15461#S4.T2.3.1.1)\.
- \[2\]C\. Belo Lourenço, D\. Cousineau, F\. Faissole, C\. Marché, D\. Mentré, and H\. Inoue\(2022\)Automated formal analysis of temporal properties of Ladder programs\.International Journal on Software Tools for Technology Transfer\.External Links:[Document](https://dx.doi.org/10.1007/s10009-022-00680-0),[Link](https://link.springer.com/article/10.1007/s10009-022-00680-0)Cited by:[§11](https://arxiv.org/html/2606.15461#S11.p2.1),[§2\.4](https://arxiv.org/html/2606.15461#S2.SS4.p1.1),[§3\.4](https://arxiv.org/html/2606.15461#S3.SS4.p1.1),[§4\.2](https://arxiv.org/html/2606.15461#S4.SS2.p2.1),[Table 2](https://arxiv.org/html/2606.15461#S4.T2.5.3.2),[itemGAP 1:](https://arxiv.org/html/2606.15461#S6.I1.i1.p1.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\.External Links:[Link](https://patents.google.com/patent/US11906943B2/en)Cited by:[§1](https://arxiv.org/html/2606.15461#S1.p1.1),[§12](https://arxiv.org/html/2606.15461#S12.p3.1),[§3\.4](https://arxiv.org/html/2606.15461#S3.SS4.p1.1),[§4\.3](https://arxiv.org/html/2606.15461#S4.SS3.p1.2),[Table 2](https://arxiv.org/html/2606.15461#S4.T2.16.14.1),[itemGAP 1:](https://arxiv.org/html/2606.15461#S6.I1.i1.p1.1),[§7\.3\.1](https://arxiv.org/html/2606.15461#S7.SS3.SSS1.p1.1),[§7\.3\.3](https://arxiv.org/html/2606.15461#S7.SS3.SSS3.p1.1)\.
- \[4\]CONTROLLINO\-PLC\(2024\)OpenPLC examples: water reserve control and staircase light control\.Note:GitHub repository \(MIT License\)Programs created 2024\-11\-13, modified 2024\-12\-05\. Hardware: CONTROLLINO MAXI Automation PLCExternal Links:[Link](https://github.com/CONTROLLINO-PLC/OpenPLC_examples)Cited by:[item 4](https://arxiv.org/html/2606.15461#S1.I1.i4.p1.1),[§7\.2](https://arxiv.org/html/2606.15461#S7.SS2.p2.1),[§8\.6](https://arxiv.org/html/2606.15461#S8.SS6.p1.1),[Table 8](https://arxiv.org/html/2606.15461#S8.T8.1.14.3),[Table 8](https://arxiv.org/html/2606.15461#S8.T8.1.15.3)\.
- \[5\]P\. Dantas, L\. C\. Cordeiro, and W\. Junior\(2026\)ESBMC\-PLC: IEC 61131\-3 ladder diagram frontend for ESBMC\.Note:GitHub Pull Request \#5322,esbmc/esbmcSource code and regression tests\. Permanently archived at Zenodo10\.5281/zenodo\.20680071\[[6](https://arxiv.org/html/2606.15461#bib.bib23)\]External Links:[Link](https://github.com/esbmc/esbmc/pull/5322)Cited by:[item 1](https://arxiv.org/html/2606.15461#S1.I1.i1.p1.1),[§1](https://arxiv.org/html/2606.15461#S1.p4.1),[§7\.1](https://arxiv.org/html/2606.15461#S7.SS1.p1.1)\.
- \[6\]P\. Dantas, L\. C\. Cordeiro, and W\. S\. Silva Júnior\(2026\)ESBMC\-PLC: formal verification of IEC 61131\-3 ladder diagram programs\.Zenodo\.Note:TACAS 2027 artefact\. Reproducible viabash conformance/run\_all\.shExternal Links:[Document](https://dx.doi.org/10.5281/zenodo.20680071),[Link](https://doi.org/10.5281/zenodo.20680071)Cited by:[§13](https://arxiv.org/html/2606.15461#S13.SSx1.p1.1),[§7\.1](https://arxiv.org/html/2606.15461#S7.SS1.p1.1),[5](https://arxiv.org/html/2606.15461#bib.bib24)\.
- \[7\]P\. Dantas, L\. Cordeiro, and W\. Junior\(2026\)ESBMC: a survey of its evolution, integration, and future directions in formal software verification\.Note:Preprint\. arXiv:2605\.26169External Links:[Link](https://arxiv.org/abs/2605.26169)Cited by:[§1](https://arxiv.org/html/2606.15461#S1.p2.1),[§12](https://arxiv.org/html/2606.15461#S12.p6.1),[§2\.3](https://arxiv.org/html/2606.15461#S2.SS3.p1.1),[Table 2](https://arxiv.org/html/2606.15461#S4.T2.16.26.2),[itemGAP 2:](https://arxiv.org/html/2606.15461#S6.I1.i2.p1.1)\.
- \[8\]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:[item 2](https://arxiv.org/html/2606.15461#S1.I1.i2.p1.1),[§1\.2](https://arxiv.org/html/2606.15461#S1.SS2.p1.1),[§10](https://arxiv.org/html/2606.15461#S10.p7.1),[§11](https://arxiv.org/html/2606.15461#S11.p3.1),[§3\.4](https://arxiv.org/html/2606.15461#S3.SS4.p1.1),[§4\.5](https://arxiv.org/html/2606.15461#S4.SS5.p1.1),[Table 2](https://arxiv.org/html/2606.15461#S4.T2.11.9.1),[§5\.1](https://arxiv.org/html/2606.15461#S5.SS1.p1.1),[Table 3](https://arxiv.org/html/2606.15461#S5.T3.2.6.6.1),[itemGAP 1:](https://arxiv.org/html/2606.15461#S6.I1.i1.p1.1),[§7\.3\.3](https://arxiv.org/html/2606.15461#S7.SS3.SSS3.p1.1),[§8\.5](https://arxiv.org/html/2606.15461#S8.SS5.p1.1)\.
- \[9\]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 \(NFM 2024\),Lecture Notes in Computer Science, Vol\.14627\.External Links:[Document](https://dx.doi.org/10.1007/978-3-031-60698-4%5F26),[Link](https://link.springer.com/chapter/10.1007/978-3-031-60698-4_26)Cited by:[§2\.4](https://arxiv.org/html/2606.15461#S2.SS4.p1.1),[§3\.3](https://arxiv.org/html/2606.15461#S3.SS3.p1.1),[Table 2](https://arxiv.org/html/2606.15461#S4.T2.15.13.1),[§7\.4\.1](https://arxiv.org/html/2606.15461#S7.SS4.SSS1.p1.1)\.
- \[10\]M\. R\. Gadelha, R\. S\. Menezes, and L\. C\. Cordeiro\(2021\-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:ISSN 1433\-2787,[Document](https://dx.doi.org/10.1007/s10009-020-00571-2)Cited by:[§1](https://arxiv.org/html/2606.15461#S1.p2.1)\.
- \[11\]N\.O\. Garanina, S\.M\. Staroletov, V\.E\. Zyubin, and I\.S\. Anureev\(2024\)Model checking programs in process\-oriented IEC 61131\-3 structured text\.Automation and Computer Sciences58\(7\),pp\. 1025–1041\.External Links:[Document](https://dx.doi.org/10.3103/S0146411624700433),[Link](https://link.springer.com/article/10.3103/S0146411624700433)Cited by:[§2\.4](https://arxiv.org/html/2606.15461#S2.SS4.p1.1),[§3\.2](https://arxiv.org/html/2606.15461#S3.SS2.p1.1),[Table 2](https://arxiv.org/html/2606.15461#S4.T2.13.11.1)\.
- \[12\]A\. Iacobelli, L\. Rinieri, A\. Melis, A\. Al Sadi, M\. Prandini, and F\. Callegati\(2024\)Detection of ladder logic bombs in PLC control programs: an architecture based on formal verification\.InProceedings of the IEEE 7th International Conference on Industrial Cyber\-Physical Systems \(ICPS 2024\),External Links:[Document](https://dx.doi.org/10.1109/ICPS59941.2024.10639995),[Link](https://ieeexplore.ieee.org/document/10639995/)Cited by:[§1](https://arxiv.org/html/2606.15461#S1.p1.1),[§10](https://arxiv.org/html/2606.15461#S10.p7.1),[§11](https://arxiv.org/html/2606.15461#S11.p2.1),[§12](https://arxiv.org/html/2606.15461#S12.p3.1),[§2\.4](https://arxiv.org/html/2606.15461#S2.SS4.p1.1),[§3\.1](https://arxiv.org/html/2606.15461#S3.SS1.p1.1),[§3\.4](https://arxiv.org/html/2606.15461#S3.SS4.p1.1),[§4\.3](https://arxiv.org/html/2606.15461#S4.SS3.p2.1),[Table 2](https://arxiv.org/html/2606.15461#S4.T2.14.12.1),[§8\.5](https://arxiv.org/html/2606.15461#S8.SS5.p1.1),[Table 8](https://arxiv.org/html/2606.15461#S8.T8.1.7.3)\.
- \[13\]J\. Lee and K\. Bae\(2024\)Formal semantics and analysis of multitask PLC ST programs with preemption\.InFormal Methods \(FM 2024\),Lecture Notes in Computer Science\.External Links:[Document](https://dx.doi.org/10.1007/978-3-031-71162-6%5F22),[Link](https://link.springer.com/chapter/10.1007/978-3-031-71162-6_22)Cited by:[§12](https://arxiv.org/html/2606.15461#S12.p5.1),[§2\.1](https://arxiv.org/html/2606.15461#S2.SS1.p2.1),[§2\.4](https://arxiv.org/html/2606.15461#S2.SS4.p1.1),[§3\.2](https://arxiv.org/html/2606.15461#S3.SS2.p1.1),[Table 2](https://arxiv.org/html/2606.15461#S4.T2.16.22.2)\.
- \[14\]J\. Lee and K\. Bae\(2025\)Formal analysis of networked PLC controllers interacting with physical environments\.InStatic Analysis Symposium \(SAS 2025\),External Links:[Document](https://dx.doi.org/10.1007/978-3-032-07106-4%5F14),[Link](https://link.springer.com/chapter/10.1007/978-3-032-07106-4_14)Cited by:[§12](https://arxiv.org/html/2606.15461#S12.p5.1),[§2\.1](https://arxiv.org/html/2606.15461#S2.SS1.p2.1),[§3\.2](https://arxiv.org/html/2606.15461#S3.SS2.p1.1),[Table 2](https://arxiv.org/html/2606.15461#S4.T2.16.25.2)\.
- \[15\]J\. Lee, S\. Kim, and K\. Bae\(2022\)Bounded model checking of PLC ST programs using rewriting modulo SMT\.InProceedings of the 8th ACM SIGPLAN International Workshop on Formal Techniques for Safety\-Critical Systems \(FTSCS 2022\),External Links:[Document](https://dx.doi.org/10.1145/3563822.3568016),[Link](https://dl.acm.org/doi/abs/10.1145/3563822.3568016)Cited by:[§2\.4](https://arxiv.org/html/2606.15461#S2.SS4.p1.1),[§3\.2](https://arxiv.org/html/2606.15461#S3.SS2.p1.1),[Table 2](https://arxiv.org/html/2606.15461#S4.T2.16.19.2)\.
- \[16\]I\. D\. Lopez\-Miguel, B\. Fernández Adiego, M\. Salinas, and C\. Betz\(2025\)Formal verification of PLCs as a service: a CERN\-GSI safety\-critical case study\.InNASA Formal Methods \(NFM 2025\),Lecture Notes in Computer Science\.Note:Extended version: arXiv:2502\.19150External Links:[Document](https://dx.doi.org/10.1007/978-3-031-93706-4%5F13)Cited by:[§2\.4](https://arxiv.org/html/2606.15461#S2.SS4.p1.1),[§3\.3](https://arxiv.org/html/2606.15461#S3.SS3.p1.1),[Table 2](https://arxiv.org/html/2606.15461#S4.T2.16.24.2),[Table 17](https://arxiv.org/html/2606.15461#S9.T17.1.5.3),[§9](https://arxiv.org/html/2606.15461#S9.p1.1)\.
- \[17\]I\. D\. Lopez\-Miguel, J\. Tournier, and B\. Fernández Adiego\(2022\)PLCverif: status of a formal verification tool for programmable logic controller\.InProc\. ICALEPCS’21,International Conference on Accelerator and Large Experimental Physics Control Systems,pp\. 248–252\.Note:arXiv:2203\.17253External Links:[Document](https://dx.doi.org/10.18429/JACoW-ICALEPCS2021-WEPV004)Cited by:[§12](https://arxiv.org/html/2606.15461#S12.p2.1),[§2\.4](https://arxiv.org/html/2606.15461#S2.SS4.p1.1),[§3\.3](https://arxiv.org/html/2606.15461#S3.SS3.p1.1),[§4\.4](https://arxiv.org/html/2606.15461#S4.SS4.p1.1),[Table 2](https://arxiv.org/html/2606.15461#S4.T2.6.4.1),[§9](https://arxiv.org/html/2606.15461#S9.p1.1),[§9](https://arxiv.org/html/2606.15461#S9.p2.1)\.
- \[18\]S\. Maesschalck, A\. Staves, R\. Derbyshire, B\. Green, and D\. Hutchison\(2023\)Walking under the ladder logic: PLC\-VBS: a PLC control logic vulnerability scanning tool\.Computers & Security127,pp\. 103116\.External Links:[Document](https://dx.doi.org/10.1016/j.cose.2023.103116),[Link](https://www.sciencedirect.com/science/article/pii/S0167404823000263)Cited by:[§3\.1](https://arxiv.org/html/2606.15461#S3.SS1.p1.1),[§3\.4](https://arxiv.org/html/2606.15461#S3.SS4.p1.1),[Table 2](https://arxiv.org/html/2606.15461#S4.T2.16.20.2)\.
- \[19\]MathWorks\(2026\)Model and generate ladder logic code for industrial tank level control system\.Note:Simulink PLC Coder Documentation \(public\)Accessed: June 2026External Links:[Link](https://www.mathworks.com/help/plccoder/ug/model-simulate-and-generate-ladder-logic-for-industrial-tank-level-control-system.html)Cited by:[item 4](https://arxiv.org/html/2606.15461#S1.I1.i4.p1.1),[§8\.6](https://arxiv.org/html/2606.15461#S8.SS6.p1.1),[§8\.6](https://arxiv.org/html/2606.15461#S8.SS6.p4.1),[Table 8](https://arxiv.org/html/2606.15461#S8.T8.1.16.3),[Table 8](https://arxiv.org/html/2606.15461#S8.T8.1.17.3)\.
- \[20\]R\. S\. Menezes, M\. Aldughaim, Farias,et al\.\(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,pp\. 376–380\.External Links:ISBN 9783031572562,ISSN 1611\-3349,[Document](https://dx.doi.org/10.1007/978-3-031-57256-2%5F24)Cited by:[§1](https://arxiv.org/html/2606.15461#S1.p2.1)\.
- \[21\]J\. Shi, Y\. Chen, Q\. Li, Y\. Huang, Y\. Yang, and M\. Zhao\(2024\)Automated test cases generator for IEC 61131\-3 structured text based dynamic symbolic execution\.IEEE Transactions on Computers73\(4\),pp\. 1048–1059\.External Links:[Document](https://dx.doi.org/10.1109/TC.2024.3351285),[Link](https://ieeexplore.ieee.org/document/10384480/)Cited by:[§4\.1](https://arxiv.org/html/2606.15461#S4.SS1.p3.1),[Table 2](https://arxiv.org/html/2606.15461#S4.T2.16.23.2)\.
- \[22\]É\. Siboulet, L\. Pottier, T\. Ranger, and B\. Riera\(2023\)Fresh approaches for structured text programmable logic controllers programs verification\.Processes11\(3\),pp\. 687\.External Links:[Document](https://dx.doi.org/10.3390/pr11030687),[Link](https://www.mdpi.com/2227-9717/11/3/687)Cited by:[§10](https://arxiv.org/html/2606.15461#S10.p1.1),[§3\.3](https://arxiv.org/html/2606.15461#S3.SS3.p1.1),[§4\.4](https://arxiv.org/html/2606.15461#S4.SS4.p1.1),[Table 2](https://arxiv.org/html/2606.15461#S4.T2.7.5.1),[§9\.5](https://arxiv.org/html/2606.15461#S9.SS5.p2.1)\.
- \[23\]R\. Sun, A\. Mera, L\. Lu, and D\. Choffnes\(2021\)SoK: attacks on industrial control logic and formal verification\-based defenses\.InProceedings of the 2021 IEEE European Symposium on Security and Privacy \(EuroS&P\),External Links:[Document](https://dx.doi.org/10.1109/EUROSP51992.2021.00034),[Link](https://ieeexplore.ieee.org/document/9581186/)Cited by:[§1](https://arxiv.org/html/2606.15461#S1.p1.1),[§3\.1](https://arxiv.org/html/2606.15461#S3.SS1.p1.1),[Table 2](https://arxiv.org/html/2606.15461#S4.T2.16.18.2),[§8\.9\.3](https://arxiv.org/html/2606.15461#S8.SS9.SSS3.p1.1)\.
- \[24\]C\. Ukegbu and H\. Mehrpouyan\(2023\)Benchmarks for the verification of safety and security properties of PLC programs in cooperative verification environments\.InProceedings of the 2023 8th International Conference on Information Systems Engineering \(ICISE 2023\),External Links:[Document](https://dx.doi.org/10.1145/3641032.3641046),[Link](https://dl.acm.org/doi/10.1145/3641032.3641046)Cited by:[§10](https://arxiv.org/html/2606.15461#S10.p7.1),[§11](https://arxiv.org/html/2606.15461#S11.p2.1),[§2\.4](https://arxiv.org/html/2606.15461#S2.SS4.p1.1),[Table 2](https://arxiv.org/html/2606.15461#S4.T2.10.8.3),[itemGAP 3:](https://arxiv.org/html/2606.15461#S6.I1.i3.p1.1)\.
- \[25\]C\. Ukegbu and H\. Mehrpouyan\(2023\)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\),External Links:[Document](https://dx.doi.org/10.1145/3576914.3587490),[Link](https://dl.acm.org/doi/10.1145/3576914.3587490)Cited by:[§10](https://arxiv.org/html/2606.15461#S10.p1.1),[§2\.4](https://arxiv.org/html/2606.15461#S2.SS4.p1.1),[§3\.3](https://arxiv.org/html/2606.15461#S3.SS3.p1.1),[§4\.4](https://arxiv.org/html/2606.15461#S4.SS4.p1.1),[Table 2](https://arxiv.org/html/2606.15461#S4.T2.8.6.1)\.
- \[26\]K\. Wang, J\. Wang, C\. M\. Poskitt, X\. Chen, J\. Sun, and P\. Cheng\(2023\)K\-ST: a formal executable semantics of the structured text language for PLCs\.IEEE Transactions on Software Engineering\.External Links:[Document](https://dx.doi.org/10.1109/TSE.2023.3315292),[Link](https://arxiv.org/abs/2202.04076)Cited by:[§12](https://arxiv.org/html/2606.15461#S12.p1.1),[§2\.2](https://arxiv.org/html/2606.15461#S2.SS2.p3.1),[§3\.2](https://arxiv.org/html/2606.15461#S3.SS2.p1.1),[§4\.4](https://arxiv.org/html/2606.15461#S4.SS4.p1.1),[§4\.5](https://arxiv.org/html/2606.15461#S4.SS5.p1.1),[Table 2](https://arxiv.org/html/2606.15461#S4.T2.16.21.2),[itemGAP 4:](https://arxiv.org/html/2606.15461#S6.I1.i4.p1.2)\.
- \[27\]M\. Weiß, P\. Marks, B\. Maschler, D\. White, P\. Kesseli, and M\. Weyrich\(2021\)Towards establishing formal verification and inductive code synthesis in the PLC domain\.InProceedings of the 19th IEEE International Conference on Industrial Informatics \(INDIN 2021\),External Links:[Document](https://dx.doi.org/10.1109/INDIN45523.2021.9557423),[Link](https://ieeexplore.ieee.org/document/9557423/)Cited by:[§1](https://arxiv.org/html/2606.15461#S1.p3.1),[§3\.1](https://arxiv.org/html/2606.15461#S3.SS1.p1.1),[Table 2](https://arxiv.org/html/2606.15461#S4.T2.16.17.2),[§8\.5](https://arxiv.org/html/2606.15461#S8.SS5.p1.1),[Table 8](https://arxiv.org/html/2606.15461#S8.T8.1.7.3)\.
- \[28\]J\. Xiong, X\. Bu, Y\. Huang, J\. Shi, and W\. He\(2021\-04\)Safety verification of iec 61131\-3 structured text programs\.IEEE Transactions on Industrial Informatics17\(4\),pp\. 2632–2640\.External Links:ISSN 1941\-0050,[Link](http://dx.doi.org/10.1109/TII.2020.2999716),[Document](https://dx.doi.org/10.1109/tii.2020.2999716)Cited by:[§2\.4](https://arxiv.org/html/2606.15461#S2.SS4.p1.1),[§3\.2](https://arxiv.org/html/2606.15461#S3.SS2.p1.1),[Table 2](https://arxiv.org/html/2606.15461#S4.T2.16.16.2)\.