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

• URL: http://arxiv.org/abs/2606.15461v1
• Date: Sat, 13 Jun 2026 20:39:49 GMT
• Title: ESBMC-PLC: Formal Verification of IEC 61131-3 Ladder Diagram Programs Using SMT-Based Model Checking
• Abstract summary: This paper presents ESBMC-PLC, the first open-source formal verifier with native LD support (PLCopen XML format)<n> ESBMC-PLC translates LD rungs to GOTO IR, models the PLC scan cycle as a while(true) proofs loop with nondeterministic inputs, and checks safety properties via bounded model checking or k-induction.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: PLCs execute safety-critical programs across industrial sectors. The dominant PLC notation, ladder diagram (LD) per IEC 61131-3, remains absent from formal verification: SMT-based model checkers cannot process LD's rung-and-coil graphics. This paper presents ESBMC-PLC, the first open-source formal verifier with native LD support (PLCopen XML format), implemented as a new ESBMC frontend. ESBMC-PLC translates LD rungs to GOTO IR, models the PLC scan cycle as a while(true) loop with nondeterministic inputs, and checks safety properties via SMT-based bounded model checking or k-induction. A five-property YAML language (mutual_exclusion, invariant, absence, response, reachability) avoids temporal logic. A survey of 22 studies (2020-2026) identifies four research gaps; ESBMC-PLC closes two of them. Evaluation on 13 benchmarks (6 domains, 3 sources - including deployed CONTROLLINO PLCs and MathWorks Simulink PLC Coder) shows correct classification across 61 properties: all 9 author-constructed programs (Categories A/B) as expected, all 4 vendor programs (Category C) correctly unlabeled, with 8 bugs found (actionable counterexamples), 7 unbounded k-induction proofs, all runs under 60ms on Apple Silicon. Feature comparison with PLCverif shows that ESBMC-PLC is the only open-source tool that combines native LD, k-induction, and SMT bit-vector semantics.

Related papers

• MemToC: Benchmarking Memory-Tool Conflict Resolution in Large Language Models [49.47300047353726]
  We introduce MemToC, a benchmark for post-tool-return arbitration with executable tools.<n>MemToC comprises 6,504 evaluation episodes constructed from 542 quality-controlled factual questions.<n>Across five open-weight 7-9B models, tool returns strongly dominate elicited closed-book answers.
  arXiv  Detail & Related papers  (2026-08-26T18:22:03Z)
• An Approach for Embedding-Guided Function Reuse Detection in Embedded C Software [1.3114114427206678]
  This paper presents a domain-aware retrieval-augmented generation pipeline for embedded software reuse detection.<n>The pipeline enriches each function by extracting its existing inline comments, callgraph context, and a project before embedding it with eight backbone models.<n>The pipeline reveals that SonarQube produces a 93.6% false-positive rate as a reuse filter, with 83.5% of failures caused by hardware-environment mismatches.
  arXiv  Detail & Related papers  (2026-08-04T18:46:17Z)
• ESBMC-PLC+: A Unified IEC 61131-3 Formal Verification Framework as a PLCverif Successor [0.0]
  ESBMC-PLC+ is the first open-source verification framework to support all three major IEC 61131-3 input formats via a single ESBMC backend.<n> ESBMC-PLC+ matches PLCverif's input coverage while providing stronger guarantees.
  arXiv  Detail & Related papers  (2026-06-22T19:13:02Z)
• ESBMC-GraphPLC: Formal Verification of Graphical PLCopen XML Ladder Diagram Programs Using SMT-Based Model Checking [0.0]
  PLCopen XML defines two encoding formats for IEC 61131-3 Ladder Diagram programs.<n> ESBMC-PLC supported the textual format but parsed graphical exports into an empty GOTO intermediate representation.<n>This paper presents ESBMC-GraphPLC, which closes this gap with a DFS-based graphical LD resolver.
  arXiv  Detail & Related papers  (2026-06-17T11:22:34Z)
• Off-the-Shelf LLMs as Process Scorers: Training-Free Alternative to PRMs for Mathematical Reasoning [51.88950852117154]
  Chunk-Level Guided Generation is a training-free alternative that uses an off-the-shelf large language model as a process scorer.<n>We show that scoring variable-length reasoning steps with large-model likelihoods is unreliable due to a systematic length bias.<n>Chunk-Level Guided Generation produces substantially shorter reasoning traces than PRM guided search.
  arXiv  Detail & Related papers  (2026-06-01T04:43:36Z)
• One Step Further: Understanding PLC Binaries Through Cross-Platform Reverse Engineering and Function-Level Semantic Analysis [7.990445011559295]
  PLC-BinX is a BCA workflow for cross-platform PLC binary understanding.<n>Under ten-fold program-level evaluation, PLC-BinX achieves 100.00% precision, recall, and F1 in toolchain prediction.<n>Results demonstrate that PLC-BinX provides an effective and interpretable approach to cross-platform PLC binary understanding.
  arXiv  Detail & Related papers  (2026-05-17T11:19:47Z)
• TSCG: Deterministic Tool-Schema Compilation for Agentic LLM Deployments [0.0]
  Production agent frameworks transmit tool schemas as MCP, a format designed for machine parsing, not for interpretation by language models.<n>For small models (4B-14B), this protocol mismatch accounts for the majority of tool-use failure at production sizes.<n>We present TSCG, a deterministic tool-schema compiler that resolves this mismatch at the API boundary.
  arXiv  Detail & Related papers  (2026-05-04T15:35:45Z)
• LFM2 Technical Report [87.58431408281973]
  We present LFM2, a family of Liquid Foundation Models designed for efficient on-device deployment and strong task capabilities.<n>The LFM2 family covers 350M-8.3B parameters, including dense models (350M, 700M, 1.2B, 2.6B) and a mixture-of-experts variant (8.3B total, 1.5B active)<n>We build multimodal and retrieval variants: LFM2-VL for vision-latency tasks, LFM2-Audio for speech, and LFM2-ColBERT for retrieval.
  arXiv  Detail & Related papers  (2025-11-28T17:56:35Z)
• Unsupervised Conformal Inference: Bootstrapping and Alignment to Control LLM Uncertainty [49.19257648205146]
  We propose an unsupervised conformal inference framework for generation.<n>Our gates achieve close-to-nominal coverage and provide tighter, more stable thresholds than split UCP.<n>The result is a label-free, API-compatible gate for test-time filtering.
  arXiv  Detail & Related papers  (2025-09-26T23:40:47Z)
• The CodeInverter Suite: Control-Flow and Data-Mapping Augmented Binary Decompilation with LLMs [43.591384969171614]
  We develop the CodeInverter Suite to improve binary decompilation.<n>We use control flow graphs and explicit data mappings to improve decompilation.<n>Our CIM-6.7B can achieve state-of-the-art decompilation performance.
  arXiv  Detail & Related papers  (2025-03-10T11:52:48Z)
• Bridging the PLC Binary Analysis Gap: A Cross-Compiler Dataset and Neural Framework for Industrial Control Systems [14.826593801448032]
  PLC-BEAD is a dataset containing 2431 compiled binaries from 700+ PLC programs across four major industrial compilers.<n>This novel dataset uniquely pairs each binary with its original Structured Text source code and standardized functionality labels.<n>We demonstrate the dataset's utility through PLCEmbed, a transformer-based framework for binary code analysis.
  arXiv  Detail & Related papers  (2025-02-27T03:27:37Z)
• EquiBench: Benchmarking Large Language Models' Reasoning about Program Semantics via Equivalence Checking [58.15568681219339]
  We introduce EquiBench, a new benchmark for evaluating large language models (LLMs)<n>This task directly tests a model's ability to reason about program semantics.<n>We evaluate 19 state-of-the-art LLMs and find that in the most challenging categories, the best accuracies are 63.8% and 76.2%, only modestly above the 50% random baseline.
  arXiv  Detail & Related papers  (2025-02-18T02:54:25Z)
• Towards Using Behavior Trees in Industrial Automation Controllers [41.94295877935867]
  The Industry 4.0 paradigm manifests the shift towards mass customization and cyber-physical production systems. There is a lack of PLC software flexibility and integration between low-level programs and high-level task-oriented control frameworks. This paper proposes an approach for improving the industrial control software design by integrating Behavior Trees into PLC programs.
  arXiv  Detail & Related papers  (2024-04-22T09:47:36Z)
• InterMPL: Momentum Pseudo-Labeling with Intermediate CTC Loss [43.39035144463951]
  Momentum PL (MPL) trains a connectionist temporal classification ( CTC)-based model on unlabeled data. CTC is well suited for MPL, or PL-based semi-supervised ASR in general, owing to its simple/fast inference algorithm and robustness against generating collapsed labels. We propose to enhance MPL by introducing intermediate loss, inspired by the recent advances in CTC-based modeling.
  arXiv  Detail & Related papers  (2022-11-02T00:18:25Z)
• K-ST: A Formal Executable Semantics of the Structured Text Language for PLCs [10.993724354322657]
  We develop K-ST, a formal executable semantics for Structured Text (ST) in the K framework. K-ST is a high-level reference semantics that can be used to evaluate the correctness and consistency of different ST implementations. We validate K-ST by executing 509 ST programs extracted from Github and comparing the results against existing commercial compilers.
  arXiv  Detail & Related papers  (2022-02-08T17:34:08Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.