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

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