ESBMC-GraphPLC: Formal Verification of Graphical PLCopen XML Ladder Diagram Programs Using SMT-Based Model Checking

• URL: http://arxiv.org/abs/2606.18941v3
• Date: Mon, 22 Jun 2026 18:37:48 GMT
• Title: ESBMC-GraphPLC: Formal Verification of Graphical PLCopen XML Ladder Diagram Programs Using SMT-Based Model Checking
• Abstract summary: 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.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: PLCopen XML defines two encoding formats for IEC 61131-3 Ladder Diagram programs: a textual encoding using <rung> elements, and a graphical encoding that represents rung logic as a directed graph of localId/refLocalId connections. ESBMC-PLC supported the textual format but parsed graphical exports from CONTROLLINO, Beremiz, and OpenPLC Editor into an empty GOTO intermediate representation, causing vacuous verification success. This paper presents ESBMC-GraphPLC, which closes this gap with a DFS-based graphical LD resolver. The resolver traverses the connection graph from leftPowerRail to each coil, extracts rung paths as Boolean contact conjunctions, and applies a three-tier I/O inference scheme. Ordering coils by rightPowerRail connectionPointIn sequence ensures SET coils process before RESET coils, matching IEC scan-cycle semantics. The graphical-to-IR conversion leaves the ESBMC backend unchanged. Validation on 3 graphical LD programs from CONTROLLINO/OpenPLC Editor shows all produce full GOTO IR with nondeterministic inputs and rung logic, versus the empty IR previously. All 3 verify SAFE at k=2 under 70ms. The 11 textual LD benchmarks are fully preserved, with no regression. Two Beremiz examples with no LD content or unsupported timer semantics are reported as discovered limitations. Artifact at Zenodo (DantasCordeiro2026graphical, doi:10.5281/zenodo.20699856).

Related papers

• PLC-Bin2Src: Retrieving Corresponding Structured Text Source Files for PLC Binaries [8.479104710721645]
  PLC developers reuse existing components and third-party libraries to reduce the cost of developing new applications.<n> binary2source matching can retrieve the corresponding Structured Text (ST) source file for a PLC binary from a candidate source repository.<n>We present PLC-Bin2Src, a cross-platform binary2source matching framework that retrieves corresponding ST source files for binaries produced by CODESYS, GEB, OpenPLC v2, and OpenPLC v3.
  arXiv  Detail & Related papers  (2026-09-08T10:52:46Z)
• Generative Diffusion Models of Stochastic Graph Signals [74.4097723209053]
  This paper tackles problems of conditional graph signal generative modeling and tackles them with a single denoising diffusion framework.<n>We learn a reverse diffusion process, parametrized by graph neural networks (GNNs), that draws graph signals conditioned directly on the graph topology and on node-feature side information.<n>We demonstrate our method on two generative tasks: stock price forecasting and optimal wireless resource allocation, with extensive numerical results in both domains.
  arXiv  Detail & Related papers  (2026-07-07T22:02:13Z)
• 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-PLC: Formal Verification of IEC 61131-3 Ladder Diagram Programs Using SMT-Based Model Checking [0.0]
  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.
  arXiv  Detail & Related papers  (2026-06-13T20:39:49Z)
• Reasoning to Align: Implicit Reasoning in Diffusion Transformers for Video Editing [55.211537893248675]
  We propose RVEDiT, an implicit Reasoning Video Editing DiT framework built around two complementary components.<n> RVEDiT consistently outperforms state-of-the-art baselines, with particularly strong gains on localized and compositional edits.
  arXiv  Detail & Related papers  (2026-05-23T17:22:14Z)
• Mapping Text to Multiplex Graph: Prompt Compression as Lévy Walk-Guided Graph Pruning [55.43705665875779]
  RAGP formulates prompt compression as Redundancy-Aware Graph Pruning on a multiplex graph.<n> Experiments on LongBench show that RAGP achieves an average score of 49.3 under a 4x compression ratio.
  arXiv  Detail & Related papers  (2026-05-04T01:41:31Z)
• Semi-supervised Instruction Tuning for Large Language Models on Text-Attributed Graphs [62.544129365882014]
  We propose a novel Semi-supervised Instruction Tuning pipeline for Graph Learning, named SIT-Graph.<n> SIT-Graph is model-agnostic and can be seamlessly integrated into any graph instruction tuning method that utilizes LLMs as the predictor.<n>Extensive experiments demonstrate that when incorporated into state-of-the-art graph instruction tuning methods, SIT-Graph significantly enhances their performance on text-attributed graph benchmarks.
  arXiv  Detail & Related papers  (2026-01-19T08:10:53Z)
• Zero-shot Graph Reasoning via Retrieval Augmented Framework with LLMs [15.558119182035995]
  We propose a new, training-free method, Graph Reasoning via Retrieval Augmented Framework (GRRAF)<n> GRRAF harnesses retrieval-augmented generation (RAG) alongside the code-generation capabilities of large language models (LLMs) to address a wide range of graph reasoning tasks.<n> Experimental evaluations on the GraphInstruct dataset reveal that GRRAF achieves 100% accuracy on most graph reasoning tasks.
  arXiv  Detail & Related papers  (2025-09-16T06:58:58Z)
• See it. Say it. Sorted: Agentic System for Compositional Diagram Generation [0.5079602839359522]
  We study sketch-to-diagram generation: converting rough hand sketches into precise, compositional diagrams.<n>We introduce See it. Say it. Sorted., a training-free agentic system that couples a Vision-Language Model (VLM) with Large Language Models (LLMs)<n>The system runs an iterative loop in which a Critic VLM proposes a small set of qualitative, edits; multiple candidate LLMs synthesize updates with diverse strategies.<n>This design prioritizes qualitative reasoning over brittle numerical estimates, preserves global constraints (e.g., alignment, connectivity), and naturally supports human-in-the-loop
  arXiv  Detail & Related papers  (2025-08-21T04:20:36Z)
• Align-GRAG: Reasoning-Guided Dual Alignment for Graph Retrieval-Augmented Generation [79.75818239774952]
  Large language models (LLMs) have demonstrated remarkable capabilities, but still struggle with issues like hallucinations and outdated information.<n>Retrieval-augmented generation (RAG) addresses these issues by grounding LLM outputs in external knowledge with an Information Retrieval (IR) system.<n>We propose Align-GRAG, a novel reasoning-guided dual alignment framework in post-retrieval phrase.
  arXiv  Detail & Related papers  (2025-05-22T05:15:27Z)
• An Efficient Post-hoc Framework for Reducing Task Discrepancy of Text Encoders for Composed Image Retrieval [34.065449743428005]
  Composed Image Retrieval (CIR) aims to retrieve a target image based on a reference image and conditioning text, enabling controllable image searches.<n>Traditional Zero-Shot (ZS) CIR methods bypass the need for expensive training CIR triplets by projecting image embeddings into the text token embedding space.<n>We introduce Reducing Taskrepancy of Texts (RTD), an efficient text-only framework that complements projection-based CIR methods.
  arXiv  Detail & Related papers  (2024-06-13T14:49:28Z)
• Visual Delta Generator with Large Multi-modal Models for Semi-supervised Composed Image Retrieval [50.72924579220149]
  Composed Image Retrieval (CIR) is a task that retrieves images similar to a query, based on a provided textual modification. Current techniques rely on supervised learning for CIR models using labeled triplets of the reference image, text, target image. We propose a new semi-supervised CIR approach where we search for a reference and its related target images in auxiliary data.
  arXiv  Detail & Related papers  (2024-04-23T21:00:22Z)
• DiagrammerGPT: Generating Open-Domain, Open-Platform Diagrams via LLM Planning [62.51232333352754]
  Text-to-image (T2I) generation has seen significant growth over the past few years. Despite this, there has been little work on generating diagrams with T2I models. We present DiagrammerGPT, a novel two-stage text-to-diagram generation framework. We show that our framework produces more accurate diagrams, outperforming existing T2I models.
  arXiv  Detail & Related papers  (2023-10-18T17:37:10Z)

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.