# Formal Verification of PLCs as a Service: A CERN-GSI Safety-Critical Case Study (extended version)

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

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 26 Feb 2025.

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

- [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)

## Abstract (arXiv)

The increased technological complexity and demand for software reliability require organizations to formally design and verify their safety-critical programs to minimize systematic failures. Formal methods are recommended by functional safety standards (e.g., by IEC 61511 for the process industry and by the generic IEC 61508) and play a crucial role. Their structured approach reduces ambiguity in system requirements, facilitating early error detection. This paper introduces a formal verification service for PLC (programmable logic controller) programs compliant with functional safety standards, providing external expertise to organizations while eliminating the need for extensive internal training. It offers a cost-effective solution to meet the rising demands for formal verification processes. The approach is extended to include modeling time-dependent, know-how-protected components, enabling formal verification of real safety-critical applications. A case study shows the application of PLC formal verification as a service provided by CERN in a safety-critical installation at the GSI particle accelerator facility.