Verification of Concurrent Software with VerCors

Concurrent software is inherently error-prone, due to the possible interactions and subtle interplays between the parallel computations. As a result, error prediction and tracing the sources of errors often is difficult. In particular, rerunning an execution with exactly the same input might not lead to the same error. To improve this situation, we need techniques that can provide static guarantees about the behaviour of a concurrent program. In this presentation, I present an approach based on program annotations, which is supported by the VerCors tool set. I will present the general set up of the approach, and discuss what kind of programs can be verified using this approach. Then I will dive into one concrete example, namely where we use the VerCors verification techniques to prove that compiler directives for program parallellisations (as done in OpenMP, for example) cannot change the behaviour of the program.