# K-ST: A Formal Executable Semantics of the Structured Text Language for PLCs

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

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 8 Feb 2022.

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

- [Agents4PLC: Automating Closed-loop PLC Code Generation and Verification in Industrial Control Systems using LLM-based Agents](https://mlsanity.com/paper/2410.14209/) (2024)
- [ESBMC-GraphPLC: Formal Verification of Graphical PLCopen XML Ladder Diagram Programs Using SMT-Based Model Checking](https://mlsanity.com/paper/2606.18941/) (2026)
- [ESBMC-PLC: Formal Verification of IEC 61131-3 Ladder Diagram Programs Using SMT-Based Model Checking](https://mlsanity.com/paper/2606.15461/) (2026)
- [ESBMC-PLC+: A Unified IEC 61131-3 Formal Verification Framework as a PLCverif Successor](https://mlsanity.com/paper/2606.23870/) (2026)
- [Detecting Ladder Logic Bombs in IEC 61131-3 PLC Programs using ESBMC-PLC+: A Formal Verification Approach with Trigger Synthesis](https://mlsanity.com/paper/2607.08417/) (2026)
- [A Benchmark Suite and Ground-Truth Methodology for Formal Verification of IEC 61131-3 Ladder Diagram Programs](https://mlsanity.com/paper/2609.18994/) (2026)

## Abstract (arXiv)

Programmable Logic Controllers (PLCs) are responsible for automating process control in many industrial systems (e.g. in manufacturing and public infrastructure), and thus it is critical to ensure that they operate correctly and safely. The majority of PLCs are programmed in languages such as Structured Text (ST). However, a lack of formal semantics makes it difficult to ascertain the correctness of their translators and compilers, which vary from vendor-to-vendor. In this work, we develop K-ST, a formal executable semantics for ST in the K framework. Defined with respect to the IEC 61131-3 standard and PLC vendor manuals, K-ST is a high-level reference semantics that can be used to evaluate the correctness and consistency of different ST implementations. We validate K-ST by executing 509 ST programs extracted from Github and comparing the results against existing commercial compilers (i.e., CODESYS, CX-Programmer, and GX Works2). We then apply K-ST to validate the implementation of the open source OpenPLC platform, comparing the executions of several test programs to uncover five bugs and nine functional defects in the compiler.