💬 NLP

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

This paper introduces ESBMC-PLC, the first open-source formal verifier that natively supports IEC 61131-3 Ladder Diagram programs by translating them into an intermediate representation for SMT-based model checking, thereby successfully verifying safety properties and detecting bugs in diverse industrial benchmarks while addressing key research gaps in the field.

Original authors: Pierre Dantas, Lucas Cordeiro, Waldir Junior

Published 2026-06-16

📖 4 min read☕ Coffee break read

CC BY 4.0

Original authors: Pierre Dantas, Lucas Cordeiro, Waldir Junior

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine a factory floor where giant machines, chemical mixers, and train signals are controlled by a tiny, tireless brain called a PLC (Programmable Logic Controller). These machines run on a special kind of instruction manual called a Ladder Diagram. Think of it like a drawing of a ladder where every "rung" is a rule: "If the red light is on AND the button is pressed, then turn on the motor."

For decades, engineers have written these rules by drawing them, not by typing code. This made it very hard for modern "safety inspectors" (formal verification tools) to check if the rules were perfect, because the inspectors only understood typed code, not drawings.

This paper introduces ESBMC-PLC, a new tool that acts like a universal translator and a super-strict safety inspector rolled into one.

Here is how it works, using simple analogies:

1. The Translator (The "Rosetta Stone")

Before this tool, you couldn't ask a computer to check a drawing. ESBMC-PLC takes the graphical "Ladder Diagram" (the drawing) and instantly translates it into a language the computer understands (a text-based intermediate code).

The Analogy: Imagine you have a recipe written in a sketchbook with pictures of ingredients. ESBMC-PLC is the chef who looks at the pictures and instantly writes out the exact text instructions: "Add 2 cups of flour, then stir." Now, the computer can read the recipe.

2. The Simulator (The "Time-Traveling Loop")

A PLC doesn't just run once; it runs in a loop, checking sensors and changing outputs thousands of times a second.

The Analogy: Most safety checks look at a single moment in time. ESBMC-PLC is like a time-traveling simulator that runs the factory's "day" over and over again. But instead of just replaying one specific day, it simulates every possible day at once. It asks: "What if the sensor breaks? What if the button is pressed twice? What if the power flickers?" It checks every single combination of events to see if a disaster can happen.

3. The "Unbounded" Proof (The "Forever Guarantee")

Old tools could only check a limited number of steps (like checking the first 100 days of a factory's life). If a bug happened on day 101, they would miss it.

The Analogy: ESBMC-PLC uses a special math trick called k-induction. Instead of counting days one by one, it proves a rule that says, "If the factory is safe today, and the rules are followed, it will be safe tomorrow, and the day after, and forever." It gives a forever guarantee that the machine will never crash, provided the rules are followed.

4. The "No-Logic" Language (The "Plain English" Checklist)

Usually, to ask a computer to check safety, you had to know complex math logic (temporal logic).

The Analogy: ESBMC-PLC lets engineers write safety rules in a simple YAML checklist (like a to-do list).
- Instead of: "For all time t, if A is true then B must be false."
- You write: "The motor and the reverse switch must never be on at the same time."
  The tool understands this plain English and checks it automatically.

What Did They Find?

The authors tested this tool on 13 different factory programs, ranging from simple motor controls to complex traffic lights and water pumps. They used programs from real-world vendors (like CONTROLLINO and MathWorks) that were not designed to be tested, just to see if the tool could handle them.

The Results:
- 100% Accuracy: It correctly identified every safe program and every unsafe program.
- Found Hidden Bugs: It found 8 specific bugs that standard testing missed. For example, it found a scenario where an emergency stop button would turn off the machine but fail to reset a timer, causing the machine to restart immediately when the button was released.
- Speed: It checked all these programs in less than 60 milliseconds (faster than a human blink).

The Bottom Line

This paper presents the first open-source tool that can take a standard industrial drawing (Ladder Diagram), translate it, and mathematically prove it is safe forever. It bridges the gap between the old-school graphical way engineers design machines and the high-tech math way computers verify safety.

Important Note: The paper claims this works for the specific "core" parts of industrial programming (Boolean logic, timers, counters). It does not yet handle complex features like floating-point numbers or advanced data arrays, but for the vast majority of safety-critical logic, it works perfectly and is ready for use today.

Technical Summary: ESBMC-PLC

Problem Statement

Programmable Logic Controllers (PLCs) are critical to industrial safety, yet the dominant programming notation, Ladder Diagram (LD) standardized in IEC 61131-3, remains largely absent from the formal verification ecosystem. While Satisfiability Modulo Theories (SMT)-based model checkers like ESBMC have matured for general-purpose software (C, Rust, Python), they cannot directly process LD's graphical "rung-and-coil" notation. Existing solutions either require manual translation to textual languages (introducing fidelity risks), rely on proprietary tools, or lack support for unbounded safety proofs. Consequently, safety-critical industrial logic often escapes the rigorous mathematical verification available to other software domains, leaving systems vulnerable to design defects and malicious code injections like Ladder Logic Bombs (LLB).

Methodology

The paper presents ESBMC-PLC, an open-source formal verifier implemented as a new frontend for the Efficient SMT-based Context-Bounded Model Checker (ESBMC). The methodology centers on a direct translation pipeline from standard PLCopen XML (the open interchange format for LD) to ESBMC's internal GOTO-Intermediate Representation (IR).

Core Architecture

Input Parsing: The tool accepts PLCopen XML files (both textual and graphical tc6_0201 formats) exported by major vendors (Siemens, Rockwell, CODESYS, OpenPLC). It reconstructs the circuit topology from reference IDs without manual editing.
Translation to GOTO-IR:
- Scan Cycle Modeling: The PLC execution model is encoded as a while(true) loop.
- State Management: Input variables are re-sampled nondeterministically at every iteration (modeling an open-world sensor environment). Output coils and internal markers are modeled as static persistent variables, preserving state across scan cycles.
- Element Mapping: LD elements (XIC/XIO contacts, OTE/OTL/OTU coils, TON/TOF/TP timers, CTU/CTD counters) are translated into GOTO-IR operations. The translation rules are designed to match the formal semantics defined by Ebnenasir [9], particularly regarding latch priority (OTL/OTU) and edge-triggered counters.
- Data Types: IEC 61131-3 types are mapped to their smallest C equivalents (e.g., BOOL to bool, TIME to uint32_t representing milliseconds).
Property Specification: A YAML-based language allows engineers to specify five types of safety properties without temporal logic expertise: mutual_exclusion, invariant, absence, response, and reachability.
Verification Engine: The backend utilizes ESBMC with the Z3 SMT solver. It supports:
- Incremental BMC: For rapid bug finding in unsafe programs.
- k-Induction: For unbounded safety proofs, verifying properties for all possible scan cycles without manual loop unrolling.

Key Contributions

First Open-Source Native LD Frontend: ESBMC-PLC is the first open-source tool to natively accept IEC 61131-3 LD programs in standard PLCopen XML format, eliminating the need for manual translation to C or ST.
Unbounded Proofs for LD: It is the first tool to apply k-induction to LD programs, enabling unbounded safety proofs rather than relying solely on bounded model checking.
Actionable Counterexamples: The tool generates counterexamples referencing original LD variable names, making them directly interpretable by automation engineers.
Systematic Gap Analysis: A survey of 22 studies (2020–2026) identified four research gaps; ESBMC-PLC directly addresses the lack of an open-source LD-to-formal translator and the absence of an ESBMC frontend for IEC 61131-3.
Benchmark Suite: The authors introduced a suite of 13 benchmarks spanning six industrial domains and three sources (original, synthetic, and real-world vendor programs), including unmodified programs from CONTROLLINO and MathWorks.

Experimental Results

The evaluation was conducted on 13 benchmarks (7 safe, 6 unsafe) across six industrial domains (motors, transport, safety, infrastructure, food industry, buildings).

Classification Accuracy: ESBMC-PLC correctly classified all 13 benchmarks with zero false positives and zero false negatives. This included 4 independent vendor programs (Category C) that were not pre-labeled by the authors.
Bug Detection: The tool identified 8 distinct bugs across the unsafe variants. These included:
- Failure to reset timers upon emergency stop (CS2).
- Reset logic overriding emergency shutdown signals (CS3).
- Missing interlocks for simultaneous phase activation in traffic lights (CS4).
- Race conditions where door open signals activated in the same scan cycle as motor start (CS8).
- Simultaneous activation of pumps and valves under sensor fault conditions (CS12).
Performance: All 61 property checks completed in under 60 ms on Apple Silicon (aarch64).
Unbounded Proofs: All 7 safe programs were verified using k-induction (converging at $k=2$ ), providing unconditional safety guarantees.
Real-World Validation: The tool successfully parsed and verified real-world programs from the CONTROLLINO repository and MathWorks Simulink PLC Coder documentation without preprocessing.

Significance and Claims

The paper claims that ESBMC-PLC demonstrates that formal verification of industrial PLC Ladder Logic is a practical, open-source, sub-second operation accessible to automation engineers.

Unique Positioning: Unlike the state-of-the-art PLCverif (which relies on CBMC and requires ST/SCL input), ESBMC-PLC is the only open-source tool combining native LD input, k-induction unbounded proofs, and SMT bit-vector semantics.
Practical Impact: By detecting bugs that conventional functional testing misses (such as sensor fault scenarios and race conditions dependent on scan-cycle ordering), the tool addresses critical safety gaps in industrial control systems.
Limitations and Scope: The authors modestly note that the translation rules are empirically validated against Ebnenasir's semantics but not formally proved equivalent to the IEC 61131-3 standard. The current implementation covers a core subset of constructs (excluding REAL/FLOAT, strings, arrays, and multi-POU programs) and does not yet support vendor-specific extensions like interrupt tasks.

The paper concludes that ESBMC-PLC closes significant research gaps in PLC verification and suggests that a unified platform integrating ESBMC-PLC's LD frontend with PLCverif's ST pipeline represents a logical future direction for industrial-grade verification.