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.