Patrick Cousot, Construction of invariance proof methods for parallel programs with sequential consistency

Patrick Cousot.
Construction of invariance proof methods for parallel programs with sequential consistency
In 27th Journées Francophones des Langages, Jade Alglave and Julien Signoles (Org.), Saint-Malo, France, January 27-30, 2016. © INRIA, 2016.
Paper:
- PDF (88 KB)
Slides of the 55mn presentation at JFLA'2016:
- 1 slide per landscape page, 148.2 Mb, 4 slides per landscape page, 148.1 Mb
Abstract:
Given a language, an operational semantics, a fixpoint definition of runtime properties, an abstraction into properties of interest, a further abstraction to express such properties of interest locally, we discuss a mathematical methodology, checkable by a proof checker, to construct an invariance proof method which is guaranteed to be sound, and depending on the appropriate choice of the abstractions, complete. Beyond proof methods, this methodology extends to all program semantics and static analyzers for parallel programs.
Keywords:
Formal methods, Program property, Invariance, Verification, Preuve, Parallel Program, Sequential consistency, Semantics, Fixpoint theorem, Fixpoint induction, Induction principle, Soundness, Completeness, Galois connection, Abstraction, Lamport proof method, Owicki-Gries proof method, Deductive methods, Static analysis.

Bibliographic reference:

@inproceedings{PCousot-JFLA-16,
  author    = {Patrick Cousot},
  title     = {Construction of invariance proof methods for parallel programs with sequential consistency},
  booktitle = {Proceedings of the 27\raisebox{0.5ex}{\scriptsize es} Journ\'ees Francophones des Langages 
               Applicatifs, JFLA 2016, Saint Malo, France, January 27--30, 2016},
  pages     = {55--61},
  year      = {2016},
  editor    = {Jade Alglave and
               Julien Signoles},
  publisher = {{INRIA}},
  url       = {http://jfla.inria.fr/2016},
}

\bibitem{PCousot-JFLA-16}
Patrick Cousot.
\newblock Construction of invariance proof methods for parallel programs with sequential consistency.
\newblock In \emph{27th Journ\'ees Francophones des Langages Applicatifs}, Jade Alglave and Julien Signoles (Eds.),
           Saint-Malo, France, 27-30 January 2016, INRIA, pp. 55--61, 2016.

copyright notice
Last modified: Thu Jan 14 09:36:22 EST 2016