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.

翻译：PLC在工业领域执行安全关键程序。作为符合IEC 61131-3标准的PLC主流表示法，梯形图（LD）始终未纳入形式化验证范畴：基于SMT的模型检测器无法处理LD的梯级-线圈图形。本文提出ESBMC-PLC——首个原生支持LD（PLCopen XML格式）的开源形式化验证工具，作为ESBMC的新前端实现。ESBMC-PLC将LD梯级转换为GOTO IR，将PLC扫描周期建模为带非确定性输入的while(true)循环，并通过基于SMT的有界模型检测或k-归纳法验证安全属性。所提出的五属性YAML语言（互斥性、不变性、不存在性、响应性、可达性）避免了时序逻辑的使用。对2020-2026年间22项研究的综述识别出四个研究空白，ESBMC-PLC填补了其中两个。在13个基准测试（覆盖6个领域、3个数据源——包括已部署的CONTROLLINO PLC和MathWorks Simulink PLC Coder）上的评估表明，其针对61个属性实现了准确分类：所有9个作者构造程序（A/B类）符合预期，全部4个供应商程序（C类）正确未标注，发现8个错误（可操作反例）、7个无界k-归纳证明，所有运行在Apple Silicon上耗时低于60ms。与PLCverif的特征对比表明，ESBMC-PLC是唯一同时集成原生LD、k-归纳法和SMT位向量语义的开源工具。