Probabilistic rely-guarantee calculus

Annabelle McIver, Tahiry Rabehaja*, Georg Struth

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

1 Citation (Scopus)


Jones’ rely-guarantee calculus for shared variable concurrency is extended to include probabilistic behaviours. We use an algebraic approach that is based on a combination of probabilistic Kleene algebra with concurrent Kleene algebra. Soundness of the algebra is shown relative to a general probabilistic event structure semantics. The main contribution of this paper is a collection of rely-guarantee rules built on top of that semantics. In particular, we show how to obtain bounds on probabilities of correctness by deriving quantitative extensions of rely-guarantee rules. The use of these rules is illustrated by a detailed verification of a simple probabilistic concurrent program: a faulty Eratosthenes sieve.

Original languageEnglish
Pages (from-to)120-134
Number of pages15
JournalTheoretical Computer Science
Publication statusPublished - 6 Dec 2016


  • Concurrency
  • Event structures
  • Kleene algebra
  • Probabilistic programs
  • Program semantics
  • Program verification
  • Rely-guarantee

Fingerprint Dive into the research topics of 'Probabilistic rely-guarantee calculus'. Together they form a unique fingerprint.

Cite this