ESOP 2015
Tue 14 - Thu 16 April 2015 London, United Kingdom
Thu 16 Apr 2015 15:00 - 15:30 at Skeel - Session 8 Chair(s): Jan Vitek

A key difficulty in verifying shared-memory concurrent programs is reasoning compositionally about each thread in isolation. Existing verification techniques for fine-grained concurrency require reasoning about static global shared resource, impeding compositionality. This paper introduces the program logic of \colosl, where each thread is verified with respect to its subjective view of the global shared state. This subjective view describes only that part of the global shared resource accessed by the thread. Subjective views may arbitrarily overlap with each other, and expand and contract depending on the resource required by the thread.

Thu 16 Apr
Times are displayed in time zone: (GMT) Azores change

14:00 - 16:00: ESOP - Session 8 at Skeel
Chair(s): Jan VitekNortheastern University
esop-2015-papers14:00 - 14:30
Cristina DavidUniversity of Oxford, Daniel KroeningUniversity of Oxford, Matt LewisUniversity of Oxford
esop-2015-papers14:30 - 15:00
esop-2015-papers15:00 - 15:30
Azalea RaadImperial College London, Jules VillardImperial College London, Philippa GardnerImperial College London
esop-2015-papers15:30 - 16:00
Filip SieczkowskiAarhus University, Kasper SvendsenAarhus University, Lars BirkedalAarhus University, Jean Pichon-PharabodUniversity of Cambridge