Jade Alglave and Patrick Cousot.<bR> Proof of mutual-exclusion and non-starvation of a program: PostgreSQL

Patrick Cousot.
Proof of mutual-exclusion and non-starvation of a program: PostgreSQL
In Dagstuhl Seminar 16471. 22 November, 2016.
Abstract:
We prove the mutual exclusion and absence of starvation of the PostgreSQL synchronization program in a weak memory model using the Alglave-Cousot proof method (POPL 2017).

Slides are available in US Letter either one slide per page PDF (1.2 Mb) or four slides per page PDF (1.2 Mb)

Bibliographic reference:

@inproceedings{AglaveAlCousot-Dagsthul-16471-2016,
  author    = {Jade Alglave and Patrick Cousot},
  title     = {Proof of mutual-exclusion and non-starvation of a program: PostgreSQL},
  booktitle = {Dagstuhl Seminar 16471},
  year      = {2016},
}

Last modified: Tue Nov 22 19:40:34 CET 2016