Counterexample analysis of formal verification methods

Nowadays, different kinds of software solutions become part of our lives more and more. A special category of software systems is the safety-critical systems. Usually a fault in a safety-critical system can lead to immersive financial loss, catastrophic environmental effect, or it can even cost human lives. Typical examples of such safety-critical systems are found in airplanes, nuclear power-plants, or even in CERN’s LHC. To ensure the safety of these systems, they are rigorously tested in an isolated, safe environment according to the strict standards regulating the development and operation of said systems. One approach of finding faults in systems is formal verification, which takes the mathematical model of the system, and mathematically proves some property on it – or provides a counterexample that demonstrates why the property does not hold. One challenge, is that the counterexample given by a verification method is usually rather long and complex, and it takes a huge amount of time to analyze it, and find the cause of the issue. The goal of my project was to find and develop methods that are capable of automatically analyze the counterexamples, and point the developers in the right directions. I implemented the algorithms using CERN’s PLCverif software, that is capable of the formal verification of PLC code.