Verification of concurrent systems with VerCors

This paper presents the VerCors approach to verification of concurrent software. It first discusses why verification of concurrent software is important, but also challenging. Then it shows how within the VerCors project we use permission-based separation logic to reason about multithreaded Java programs. We discuss in particular how we use the logic to use different implementations of synchronisers in verification, and how we reason about class invariance properties in a concurrent setting. Further, we also show how the approach is suited to reason about programs using a different concurrency paradigm, namely kernel programs using the Single Instruction Multiple Data paradigm. Concretely, we illustrate how permission-based separation logic is suitable to verify functional correctness properties of OpenCL kernels. All verification techniques discussed in this paper are supported by the VerCors tool set