ESBMC-PLC+: A UNIFIED IEC 61131-3 FORMAL VERIFICATION FRAMEWORK AS A PLCVERIF SUCCESSOR

Formal verification is essential for ensuring the safety of Programmable Logic Controllers (PLCs) in critical infrastructure like nuclear plants and railway systems. While PLCverif is the industry standard for open-source PLC verification, it suffers from three major limitations: it lacks native support for the dominant Ladder Diagram (LD) notation, relies on bounded model checking (which cannot prove safety for all future cycles), and struggles with state-space explosion when verifying programs containing integer-based timers or counters.

ESBMC-PLC+ addresses these gaps by creating a unified pipeline that routes all IEC 61131-3 formats into the ESBMC model checker. The framework introduces two primary technical contributions:

1. Structured Text (ST) Frontend: It utilizes the MATIEC compiler to translate ST/SCL code into C, which is then wrapped with nondeterministic input modeling and property injection to leverage ESBMC's powerful k-induction engine.
2. Graphical LD Function Block Semantics: It extends the existing Depth-First Search (DFS) resolver to correctly model persistent state variables for common function blocks (timers like TON/TOF, counters like CTU/CTD, and edge triggers). These are encoded into the GOTO Intermediate Representation (IR), allowing the backend to reason about them as state-cycle variables rather than opaque nodes.

By unifying these frontends, ESBMC-PLC+ provides the first open-source tool capable of performing unbounded safety proofs across the full spectrum of IEC 61131-3 languages. Experimental results demonstrate that the framework is not only more versatile than PLCverif but also significantly more efficient. In benchmarks involving integer-valued timers, ESBMC-PLC+ completed proofs in seconds where the nuXmv BDD backend timed out at 120 seconds, demonstrating a 400-2,000x performance improvement.