22 citations · 40 across the 16 of their papers we have counts for
14 papers · 1 filter
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…
Differential Testing of a Verification Framework for Compiler Optimizations (Experience Paper)
Mark Utting, Brae J. Webb, Ian J. Hayes
We want to verify the correctness of optimization phases in the GraalVM compiler, which consist of many thousands of lines of complex Java code performing sophisticated graph trans…
Contextuality in distributed systems
Nasos Evangelou-Oost, Callum Bannister, Ian J. Hayes
We present a lattice of distributed program specifications, whose ordering represents implementability/refinement. Specifications are modelled by families of subsets of relative ex…
A Formal Semantics of the GraalVM Intermediate Representation
Brae J. Webb, Mark Utting, Ian J. Hayes
The optimization phase of a compiler is responsible for transforming an intermediate representation (IR) of a program into a more efficient form. Modern optimizers, such as that us…
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…