3 papers
cs.LO2019
Handling localisation in rely/guarantee concurrency: An algebraic approach
Larissa A. Meinicke, Ian J. Hayes
The rely/guarantee approach of Jones extends Hoare logic with rely and guarantee conditions in order to allow compositional reasoning about shared-variable concurrent programs. Thi…
cs.LO2018
Encoding fairness in a synchronous concurrent program algebra: extended version with proofs
Ian J. Hayes, Larissa A. Meinicke
Concurrent program refinement algebra provides a suitable basis for supporting mechanised reasoning about shared-memory concurrent programs in a compositional manner, for example,…
cs.LO2017
A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency
Ian J. Hayes, Larissa A. Meinicke, Kirsten Winter +1
This research started with an algebra for reasoning about rely/guarantee concurrency for a shared memory model. The approach taken led to a more abstract algebra of atomic steps, i…