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

In this paper we propose a new proof system, iCAP-TSO, that captures this fiction formally, for a language with a TSO memory model. The logic supports reasoning about libraries that directly exploit the relaxed memory model to achieve maximum efficiency. When these libraries provide sufficient guarantees, the logic hides the underlying complexity and admits standard separation logic rules for reasoning about their more high-level clients.

Thu 16 Apr

Displayed time zone: Azores change

14:00 - 16:00
Session 8ESOP at Skeel
Chair(s): Jan Vitek Northeastern University
14:00
30m
Talk
Propositional Reasoning about Safety and Termination of Heap-Manipulating Programs
ESOP
Cristina David University of Oxford, Daniel Kroening University of Oxford, Matt Lewis University of Oxford
14:30
30m
Talk
Full reduction in the face of absurdity
ESOP
15:00
30m
Talk
CoLoSL: Concurrent Local Subjective Logic
ESOP
Azalea Raad Imperial College London, Jules Villard Imperial College London, Philippa Gardner Imperial College London
15:30
30m
Talk
A Separation Logic for Fictional Sequential Consistency
ESOP
Filip Sieczkowski Aarhus University, Kasper Svendsen Aarhus University, Lars Birkedal Aarhus University, Jean Pichon-Pharabod University of Cambridge