Related papers: ESBMC-PLC+: A Unified IEC 61131-3 Formal Verification Framework as a PLCverif Successor

ESBMC-PLC+: A Unified IEC 61131-3 Formal Verification Framework as a PLCverif Successor

URL: http://arxiv.org/abs/2606.23870v2
Date: Wed, 24 Jun 2026 10:18:33 GMT
Title: ESBMC-PLC+: A Unified IEC 61131-3 Formal Verification Framework as a PLCverif Successor
Abstract summary: 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.
Score: 0.0
License: http://creativecommons.org/licenses/by/4.0/
Abstract: PLCverif is the most mature open-source platform for PLC formal verification, developed at CERN and in production use since 2019. Yet it has two fundamental limitations: no support for Ladder Diagram (LD) programs, the dominant PLC notation, and reliance on CBMC as its primary backend, which restricts verification to bounded proofs. The PLCverif authors themselves identified ESBMC as the appropriate backend improvement. Prior work established ESBMC-PLC (a textual LD frontend with k-induction) and ESBMC-GraphPLC (graphical PLCopen XML support); together, they cover LD with unbounded proofs but not Structured Text (ST), and graphical LD with timer/counter function blocks remains unverifiable. This paper presents ESBMC-PLC+, a unified framework that closes both gaps: (1) an ST/SCL frontend via the MATIEC IEC 61131-3 compiler, routing C-compiled ST to ESBMC with nondeterministic input modeling and YAML property injection; (2) function block state semantics for graphical LD, extending the DFS resolver to model TON/TOF/TP timers, CTU/CTD counters, and R_TRIG/F_TRIG edge triggers as persistent scan-cycle state variables in the GOTO IR. ESBMC-PLC+ is the first open-source PLC verification framework to support all three major IEC 61131-3 input formats via a single ESBMC backend, enabling k-induction-unbounded safety proofs. A feature comparison with PLCverif and experimental evaluation on 8 benchmark programs, including programs with up to 8 integer timers, shows that ESBMC-PLC+ matches PLCverif's input coverage while providing stronger guarantees. Against nuXmv's BDD backend, ESBMC-PLC+ is 400-2,000x faster on timer programs and completes proofs where nuXmv BDD times out at 120s.

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)
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)
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)
TempRet: Temporal Enhancement and Two-Stage Reranking for CVPR 2026 EPIC-KITCHENS-100 Multi-Instance Retrieval Challenge [71.10535279591527]
We present our solution, termed TempRet, to the CVPR 2026 EPIC-KITCHENS-100 MIR challenge.<n>Our approach builds upon a CLIP-based dual-encoder backbone and introduces two key components to address the temporal and cross-modal challenges.<n>Our method achieves 67.97% average mAP and 82.92% average nDCG on the EK-100 MIR benchmark.
arXiv Detail & Related papers (2026-05-23T08:37:39Z)
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)
GLM-OCR Technical Report [65.42028025507491]
GLM-OCR is an efficient compact model designed for real-world document understanding.<n>It combines a CogViT visual encoder with a GLM language decoder, achieving a strong balance between computational efficiency and recognition performance.<n>Extensive evaluations on public benchmarks and industrial scenarios show that GLM-OCR achieves competitive or state-of-the-art performance.
arXiv Detail & Related papers (2026-03-11T15:55:47Z)
FluxMem: Adaptive Hierarchical Memory for Streaming Video Understanding [49.23912975740968]
FluxMem adaptively compresses redundant visual memory through a hierarchical, two-stage design.<n>It achieves new state-of-the-art results on existing online video benchmarks.<n>It maintains strong offline performance, achieving 73.1 on MLVU while using 65% fewer visual tokens.
arXiv Detail & Related papers (2026-03-02T17:16:47Z)
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)
Preserving Cross-Modal Consistency for CLIP-based Class-Incremental Learning [77.82901519692378]
Class-incremental learning (CIL) enables models to continuously learn new categories from sequential tasks without forgetting previously acquired knowledge.<n>We propose DMC, a two-stage framework for CLIP-based CIL that decouples the adaptation of the vision encoder and the optimization of textual soft prompts.<n>Extensive experiments on CIFAR-100, Imagenet-R, CUB-200, and UCF-101 demonstrate that both DMC and DMC-OT achieve state-of-the-art performance.
arXiv Detail & Related papers (2025-11-14T05:36:36Z)
Towards Effective and Efficient Non-autoregressive Decoding Using Block-based Attention Mask [74.64216073678617]
AMD performs parallel NAR inference within contiguous blocks of output labels concealed using attention masks. A beam search algorithm is designed to leverage a dynamic fusion of CTC, AR Decoder, and AMD probabilities. Experiments on the LibriSpeech-100hr corpus suggest the tripartite Decoder incorporating the AMD module produces a maximum decoding speed-up ratio of 1.73x.
arXiv Detail & Related papers (2024-06-14T13:42:38Z)
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)

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