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

arXiv: https://arxiv.org/abs/2606.15461 · HTML: https://mlsanity.com/paper/2606.15461/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 6 of its 29 references that are in the map.
- First posted on arXiv 13 Jun 2026.

## Builds on (most cited first, 6 of 6)

- [K-ST: A Formal Executable Semantics of the Structured Text Language for PLCs](https://mlsanity.com/paper/2202.04076/) (2022)
- [PLCverif: Status of a Formal Verification Tool for Programmable Logic Controller](https://mlsanity.com/paper/2203.17253/) (2022)
- [SoK: Attacks on Industrial Control Logic and Formal Verification-Based Defenses](https://mlsanity.com/paper/2006.04806/) (2020)
- [Towards establishing formal verification and inductive code synthesis in the PLC domain](https://mlsanity.com/paper/2106.15878/) (2021)
- [Formal Verification of PLCs as a Service: A CERN-GSI Safety-Critical Case Study (extended version)](https://mlsanity.com/paper/2502.19150/) (2025)
- [ESBMC: A Survey of Its Evolution, Integration, and Future Directions in Formal Software Verification](https://mlsanity.com/paper/2605.26169/) (2026)

## Built on by (most cited first, 1 of 1)

- [ESBMC-GraphPLC: Formal Verification of Graphical PLCopen XML Ladder Diagram Programs Using SMT-Based Model Checking](https://mlsanity.com/paper/2606.18941/) (2026)

## Abstract (arXiv)

PLCs execute safety-critical programs across industrial sectors. The dominant PLC notation, ladder diagram (LD) per IEC 61131-3, remains absent from formal verification: SMT-based model checkers cannot process LD's rung-and-coil graphics. This paper presents ESBMC-PLC, the first open-source formal verifier with native LD support (PLCopen XML format), implemented as a new ESBMC frontend. ESBMC-PLC translates LD rungs to GOTO IR, models the PLC scan cycle as a while(true) loop with nondeterministic inputs, and checks safety properties via SMT-based bounded model checking or k-induction. A five-property YAML language (mutual_exclusion, invariant, absence, response, reachability) avoids temporal logic. A survey of 22 studies (2020-2026) identifies four research gaps; ESBMC-PLC closes two of them. Evaluation on 13 benchmarks (6 domains, 3 sources - including deployed CONTROLLINO PLCs and MathWorks Simulink PLC Coder) shows correct classification across 61 properties: all 9 author-constructed programs (Categories A/B) as expected, all 4 vendor programs (Category C) correctly unlabeled, with 8 bugs found (actionable counterexamples), 7 unbounded k-induction proofs, all runs under 60ms on Apple Silicon. Feature comparison with PLCverif shows that ESBMC-PLC is the only open-source tool that combines native LD, k-induction, and SMT bit-vector semantics.