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

Jade Alglave and Patrick Cousot.
Proof of mutual-exclusion and non-starvation of a program: PostgreSQL
In The 2016 workshop on Analysis and Verification of Dependable Cyber Physical Software Changsha, China, December 09, 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 (35.3 Mb) or four slides per page PDF (34.8 Mb)

Bibliographic reference:

@inproceedings{AglaveCousot-AVDCPS-2016,
  author    = {Jade Alglave and Patrick Cousot},
  title     = {Proof of mutual-exclusion and non-starvation of a program: PostgreSQL},
  booktitle = {The 2016 workshop on Analysis and Verification of Dependable Cyber Physical 
               Software Changsha, China},
  year      = {December 9, 2016},
}

Last modified: Sat Dec 31 07:36:38 EST 2016