Verification of Concurrent Software: Java and OpenCL
This talk presents the VerCors approach to verification of concurrent software. First we discuss why verification of concurrent software is important, but also challenging, and we show how permission-based separation logic allows one to reason about concurrent programs in a thread-modular way. We show how we extend the logic to reason about functional properties of Java programs in a concurrent setting. Further, we also show how the approach is used to reason about kernel programs using the Single Instruction Multiple Data paradigm. Concretely, we illustrate how permission-based separation logic is used to verify functional correctness properties of OpenCL kernels.