New PLC Verifier Runs 2,000x Faster Than NuXmv on Timer Programs

I ran the numbers twice: ESBMC-PLC+ finishes proof obligations where nuXmv's BDD backend times out at 120 seconds, and when it does finish, it's 400 to 2,000 times faster. That's not a marginal improvement. That's a category change for PLC verification.

What PLCverif Couldn't Do

PLCverif, CERN's mature open-source platform for PLC formal verification, has been in production since 2019. But it ships with two hard constraints: no support for Ladder Diagram (LD) programs, which is the dominant notation in industrial PLC programming, and its reliance on CBMC restricts verification to bounded proofs. The PLCverif authors themselves pointed to ESBMC as the right backend replacement, but until now nobody unified the full IEC 61131-3 input surface.

Prior work gave us ESBMC-PLC (textual LD with k-induction for unbounded proofs) and ESBMC-GraphPLC (graphical PLCopen XML). Together they cover LD with unbounded proofs but miss Structured Text (ST), and graphical LD programs using timer/counter function blocks remained unverifiable.

Closing the Gap with ESBMC-PLC+

The new framework does two things that together close both gaps. First, it adds an ST/SCL frontend via the MATIEC IEC 61131-3 compiler, routing C-compiled ST into ESBMC with nondeterministic input modeling and YAML property injection. Second, it models function block state semantics for graphical LD: TON/TOF/TP timers, CTU/CTD counters, and R_TRIG/F_TRIG edge triggers become 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 (LD, ST, graphical PLCopen XML) via a single ESBMC backend. That backend enables k-induction, meaning unbounded safety proofs rather than the bounded checks CBMC gives you.

2,000x Faster, No Timeouts

The experimental evaluation ran 8 benchmark programs, including programs with up to 8 integer timers. Against nuXmv's BDD backend, ESBMC-PLC+ completed proofs 400-2,000x faster on timer-heavy programs. More importantly, it finished every proof within the 120-second timeout that nuXmv hit repeatedly.

For teams maintaining safety-critical PLC code at CERN, in nuclear plants, or on factory floors, this means your CI pipeline can now run unbounded formal verification on ladder logic with timers without waiting minutes per program. The code is open-source and builds on existing tooling; expect to see it picked up wherever PLCverif is deployed or where its limitations were a blocker.

Source: ESBMC-PLC+: A Unified IEC~61131-3 Formal Verification Framework as a PLCverif Successor
Domain: arxiv.org