POPL 2017
Sun 15 - Sat 21 January 2017
Wed 18 Jan 2017 10:30 - 10:55 at Amphitheater 44 - Abstract Interpretation Chair(s): Isabella Mastroeni

We design an invariance proof method for concurrent programs parameterised by a weak consistency model. This generalises Lamport/Owicki-Gries methods for sequential consistency. The calculational design of the proof method by abstract interpretation of a truly parallel semantics with separate communications restricted by a communication specification ensures soundness and (relative) completeness. We use the cat language to write specifications of consistency models as well as concurrent program specifications. We show how to design minimal program-specific communication specifications ensuring correctness which can be ported to different architectures by refencing.

Wed 18 Jan
Times are displayed in time zone: (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:10: POPL - Abstract Interpretation at Amphitheater 44
Chair(s): Isabella MastroeniUniversity of Verona, Italy
POPL-2017-papers10:30 - 10:55
Jade AlglaveUniversity College London, Patrick CousotNew York University
POPL-2017-papers10:55 - 11:20
Kimball GermaneUniversity of Utah, Matthew MightUniversity of Utah; Harvard Medical School; The White House
POPL-2017-papers11:20 - 11:45
Huisong LiINRIA/CNRS/ENS/PSL*, François BérengerINRIA/CNRS/ENS/PSL*, Bor-Yuh Evan ChangUniversity of Colorado Boulder, Xavier RivalINRIA/CNRS/ENS Paris
POPL-2017-papers11:45 - 12:10
Gagandeep SinghETH Zurich, Switzerland, Markus PüschelETH Zurich, Martin VechevETH Zurich