ECOOP 2015
Sun 5 - Fri 10 July 2015 Prague, Czech Republic
Tue 7 Jul 2015 14:45 - 15:35 at Hluboka I - Invited Talk Chair(s): Rosemary Monahan

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.

Tue 7 Jul

FTfJP-2015-papers
14:45 - 15:35: FTfJP - Invited Talk at Hluboka I
Chair(s): Rosemary Monahan
FTfJP-2015-papers143627310000014:45 - 15:35
Talk