K-ESBMC: An Executable Formal Semantics of IEC 61131-3 Ladder Diagram for Validating Verifier Translations

Jul 16, 2026

Upload by Levi

Automated verifiers for IEC 61131-3 Ladder Diagram (LD) improve safety by turning diagrams into model-checker inputs. Yet unverified front-end translations may diverge from the standard, silently missing violations or creating false alarms. K-ESBMC introduces executable formal semantics of IEC 61131-3 LD in the K framework. It provides an interpreter and deductive verifier from one definition, models key LD constructs and the retentive scan cycle, and validates translations via differential testing against OpenPLC/MATIEC and other verifiers.

LanguageEnglish

CategoryResearch & Report

FormatPDF

Pages19

Reading Time48 min

Introduction

The Trust Gap

An Executable Reference Semantics

Grounding and Using the Semantics

K-ESBMC: AN EXECUTABLE FORMAL SEMANTICS OF IEC 61131-3 LADDER DIAGRAM FOR VALIDATING VERIFIER TRANSLATIONS A PREPRINT Pierre Dantas* Department of Computer Science The University of Manchester Manchester, UK [pierre.dantas@manchester.ac.uk](pierre.dantas@manchester.ac.uk)[ ](pierre.dantas@manchester.ac.uk)ORCID: 0000-0001-6390-9340 Lucas Cordeiro* Department of Computer Science The University of Manchester Manchester, UK [lucas.cordeiro@manchester.ac.uk](lucas.cordeiro@manchester.ac.uk)[ ](lucas.cordeiro@manchester.ac.uk)ORCID: 0000-0002-6235-4272 arXiv :2607 . 10499v 1 [ cs .PL] 11 Jul 2026 Waldir Junior* Electrical Engineering Federal University of Amazonas (UFAM) Manaus, AM, Brazil [waldirjr@ufam.edu.br](waldirjr@ufam.edu.br) ORCID: 0000-0003-3095-0042 July 2026 ABSTRACT Automated verifiers for IEC 61131-3 Ladder Diagram (LD) enhance safety by translating diagrams into model-checker inputs. Still, their unverified front-end translations risk silently returning incorrect results (missing violations or raising false alarms) when they diverge from the standard. We address this gap with K-ESBMC, an executable formal semantics of IEC 61131-3 LD built in the K framework. K-ESBMC models contacts, coils, timers, counters, edge blocks, and the retentive scan cycle, generating both an interpreter and a deductive verifier from a single definition. Validated scan-for-scan against OpenPLC/MATIEC; K-ESBMC serves as an independent reference oracle to test the ESBMC-PLC LD→GOTO translation differentially. It agrees with ESBMC on most programs and reproduces injected violations with concrete witnesses. Every disagreement exposesa genuine ESBMC defect – confirmed by OpenPLC and two other verifiers – revealing two failure modes: an unsound skip that certifies unsafe programs, and an imprecise havoc that produces spurious counterexamples. For the combinational and latch fragment, we machine-check in kprove that K-ESBMC ’s rules implement the standard’s input/output relation, elevating the correctness argument from empirical to formal. K-ESBMC provides a reusable, standard-faithful oracle for auditing any LD verifier’s translation, offering a general approach to verifying the soundness of translation-based verification tools. Keywords executable formal semantics · K framework · IEC 61131-3 · Ladder Diagram · PLC · reference oracle · differential testing · translation validation · scan cycle · function blocks · ESBMC · BMC · model checking · OpenPLC · PLCopen XML ∗The authors contributed equally to this research. 1 Introduction Programmable Logic Controllers (PLCs) run much of the world’s safety-critical automation, and Ladder Diagram (LD)– the graphical, relay-inspired notation of International Electrotechnical Commission (IEC) 61131-3 – remains the language in which that logic is most often written and certified. Because a PLC fault can injure people or damage a plant, LD programs are natural targets for formal verification. A line of automated tools now checks safety properties of IEC 61131-3 programs by translating them into the input language of a model checker. The ESBMC-PLC family [6, 7, 8], for instance, lowers an LD diagram into a GOTO Intermediate Representation (IR) and discharges the resulting verification conditions with Satisfiability Modulo Theories (SMT)-based Bounded Model Checking (BMC) and k-induction. 1.1 The Trust Gap Every such tool rests on an unstated assumption: that its front-end – the translation from the diagram to the verifier’s model – faithfully reflects IEC 61131-3. A verifier is only as sound as this translation, yet the translation is itself unverified code. In the ESBMC-PLC line, the LD→GOTO rules were designed to match an informal reference formalization, but were never proven equivalent to the standard. When the translation and the standard disagree, theverifier can silently return the wrong answer: it can certify a hazardous program as safe (if the translation

FAQs

What problem does K-ESBMC address in IEC 61131-3 LD verification tools?

It addresses the trust gap where LD-to-verifier translations may not faithfully match the IEC 61131-3 standard, leading to missed violations or false alarms.

How does K-ESBMC work at a high level?

It defines an executable formal semantics for IEC 61131-3 LD in the K framework, generating both an interpreter and a deductive verifier from the same rewrite-rule definition.

How is K-ESBMC used to validate translation-based verification results?

It is validated scan-for-scan against OpenPLC/MATIEC, then used as an independent reference oracle for differential testing of ESBMC-PLC’s LD→GOTO translation, including reproduction of injected violations with concrete witnesses.

Jul 16, 2026

Upload by Levi