Ogre and Pythia: an invariance proof method for weak consistency models

DOI10.1145/3009837.3009883zbMath1380.68101OpenAlexW2562986368MaRDI QIDQ5370841

Patrick Cousot, Jade Alglave

Publication date: 20 October 2017

Published in: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL: https://discovery.ucl.ac.uk/id/eprint/1550683/

zbMATH Keywords

verificationinvarianceconcurrencyweak consistency modelsdistributed and parallel programming

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (7)

Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL ⋮ Unifying Operational Weak Memory Verification: An Axiomatic Approach ⋮ Unnamed Item ⋮ Reasoning about promises in weak memory models with event structures ⋮ A fine-grained semantics for arrays and pointers under weak memory models ⋮ Robustness Against Transactional Causal Consistency. ⋮ Checking robustness between weak transactional consistency models

This page was built for publication: Ogre and Pythia: an invariance proof method for weak consistency models