Feb 23, 2016: Marieke Huisman: Verification of Concurrent Software

February 23, 2016Verification of Concurrent Software
Room: HB 2FMarieke Huisman

This talk presents the VerCors approach to verification of concurrent software. In this talk, I will show you some of the highlights of what we achieved during the 5 years of the VerCors project.
First I discuss why verification of concurrent software is important, but also challenging, and I will show how permission-based separation logic allows one to reason about multithreaded Java programs in a thread-modular way. I will briefly discuss the different permission systems that we use (fractional permissions vs. symbolic permissions). I will also discuss how we extend the logic to reason about functional properties in a concurrent setting, using the notion of histories and futures. Further, I will show how the approach is also suited to reason about programs using a different concurrency paradigm, namely kernel programs using the Single Instruction Multiple Data paradigm. Concretely, I will illustrate how permission-based separation logic is used to verify functional correctness properties of OpenCL kernels.