Trace Based Semantics for Rely Guarantee

Marialena Hadjikosti, Andrei Popescu 📧 and Jamie Wright 📧

August 11, 2026

Abstract

We formalize a trace-based Rely-Guarantee semantics based on the work of Xu et al. The foundation includes an abstract Sequential/While/Parallel programming language equipped with operational semantics designed for concurrent reasoning. Upon this, we build a reasoning infrastructure that includes Rely-Guarantee inversion rules, alongside abstract definitions and standard soundness proofs for both unary and binary settings.

License

BSD License

Topics

Related publications

Session Trace_Based_Rely_Guarantee

Cite

× 
@article{Trace_Based_Rely_Guarantee-AFP,
  author  = {Marialena Hadjikosti and Andrei Popescu and Jamie Wright},
  title   = {Trace Based Semantics for Rely Guarantee},
  journal = {Archive of Formal Proofs},
  month   = {August},
  year    = {2026},
  note    = {\url{https://isa-afp.org/entries/Trace_Based_Rely_Guarantee.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download