Successful collaboration with CERN

Our research group successfully collaborated with CERN on the architecture design and integration of an automated tool serving for formal verification of the source code of Programmable Logic Controllers.

Our Theta framework was integrated as a verification back-end into the PLCverif tool of CERN, the European Organization for Nuclear Research. An extensive benchmarking session on 90 input PLC programs concluded that it can verify all of them.