13 citations · 52 across the 27 of their papers we have counts for
15 papers · 1 filter
Reasoning about Promises in Weak Memory Models with Event Structures (Extended Version)
Heike Wehrheim, Lara Bargmann, Brijesh Dongol
Modern processors such as ARMv8 and RISC-V allow executions in which independent instructions within a process may be reordered. To cope with such phenomena, so called promising se…
Verifying C11-Style Weak Memory Libraries via Refinement
Sadegh Dalvandi, Brijesh Dongol
Deductive verification of concurrent programs under weak memory has thus far been limited to simple programs over a monolithic state space. For scalability, we also require modular…
Owicki-Gries Reasoning for C11 Programs with Relaxed Dependencies (Extended Version)
Daniel Wright, Mark Batty, Brijesh Dongol
Deductive verification techniques for C11 programs have advanced significantly in recent years with the development of operational semantics and associated logics for increasingly…
Proceedings 18th Refinement Workshop
John Derrick, Brijesh Dongol, Steve Reeves
Refinement is one of the cornerstones of a formal approach to software engineering. Refinement is the process of developing a more detailed design or implementation from an abstrac…
Causal Linearizability: Compositionality for Partially Ordered Executions
Simon Doherty, John Derrick, Brijesh Dongol +1
In the interleaving model of concurrency, where events are totally ordered, linearizability is compositional: the composition of two linearizable objects is guaranteed to be linear…
Convolution Algebras: Relational Convolution, Generalised Modalities and Incidence Algebras
Brijesh Dongol, Ian J. Hayes, Georg Struth
Convolution is a ubiquitous operation in mathematics and computing. The Kripke semantics for substructural and interval logics motivates its study for quantale-valued functions rel…