22 citations · 44 across the 15 of their papers we have counts for
15 papers
Distributive Laws for Parallel Composition in Rely-Guarantee Concurrency
Ian J. Hayes, Larissa A. Meinicke
The rely/guarantee approach supports the stepwise development of concurrent programs. Our goal is to develop a theory for reasoning algebraically about concurrent programs in a rel…
Reasoning about concurrent loops and recursion with rely-guarantee rules
Ian J. Hayes, Larissa A. Meinicke, Cliff B. Jones
The objective of this paper is to present general, mechanically verified, refinement rules for reasoning about recursive programs and while loops in the context of concurrency. We…
Reasoning about expression evaluation under interference
Ian J. Hayes, Cliff B. Jones, Larissa A. Meinicke
Hoare-style inference rules for program constructs permit the copying of expressions and tests from program text into logical contexts. It is known that this requires care even for…
Practical Rely/Guarantee Verification of an Efficient Lock for seL4 on Multicore Architectures
Robert J. Colvin, Ian J. Hayes, Scott Heiner +3
Developers of low-level systems code providing core functionality for operating systems and kernels must address hardware-level features of modern multicore architectures. A partic…
Restructuring a concurrent refinement algebra
Ian J. Hayes, Larissa A. Meinicke, Naso Evangelou-Oost
The concurrent refinement algebra has been developed to support rely/guarantee reasoning about concurrent programs. The algebra supports atomic commands and defines parallel compos…
Data reification in a concurrent rely-guarantee algebra
Larissa A. Meinicke, Ian J. Hayes, Cliff B. Jones
Specifications of significant systems can be made short and perspicuous by using abstract data types; data reification can provide a clear, stepwise, development history of program…
Reasoning about distributive laws in a concurrent refinement algebra
Larissa A. Meinicke, Ian J. Hayes
Distributive laws are important for algebraic reasoning in arithmetic and logic. They are equally important for algebraic reasoning about concurrent programs. In existing theories…
Trace models of concurrent valuation algebras
Naso Evangelou-Oost, Larissa Meinicke, Callum Bannister +1
This paper introduces Concurrent Valuation Algebras (CVAs), a novel extension of ordered valuation algebras (OVAs). CVAs include two combine operators representing parallel and seq…
Deriving Laws for Developing Concurrent Programs in a Rely-Guarantee Style
Ian J. Hayes, Larissa A. Meinicke, Patrick A. Meiring
This paper presents a theory for the refinement of shared-memory concurrent algorithms from specifications. We augment pre and post condition specifications with Jones' rely and gu…
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…
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,…
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…
An algebra of synchronous atomic steps
Ian J. Hayes, Robert Colvin, Larissa Meinicke +2
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…
Hidden-Markov Program Algebra with iteration
Annabelle McIver, Larissa Meinicke, Carroll Morgan
We use Hidden Markov Models to motivate a quantitative compositional semantics for noninterference-based security with iteration, including a refinement- or "implements" relation t…
Compositional closure for Bayes Risk in probabilistic noninterference
Annabelle McIver, Larissa Meinicke, Carroll Morgan
We give a sequential model for noninterference security including probability (but not demonic choice), thus supporting reasoning about the likelihood that high-security values mig…