PLCverif: Status of a Formal Verification Tool for Programmable Logic Controller


PLCverif was first released internally for CERN usage in 2019 and is available to everyone since September 2020 via an open source licence. In this paper, we will first give an overview of the PLCverif platform capabilities before focusing on the improvements done since 2019 such as the larger support coverage of the Siemens PLC programming languages, the better support of the C Bounded Model Checker backend (CBMC) and the process of releasing PLCverif as an open-source software.

In the 18th International Conference on Accelerator and Large Experimental Physics Control Systems
Ignacio D. Lopez-Miguel
Ignacio D. Lopez-Miguel
PhD student

I am a PhD student at the Technical University of Vienna (TU Wien)