76 citations · 129 across the 23 of their papers we have counts for
5 papers · 1 filter
View-Based Axiomatic Reasoning for PSO (Extended Version)
Lara Bargmann, Heike Wehrheim
Weak memory models describe the semantics of concurrent programs on modern multi-core architectures. Reasoning techniques for concurrent programs, like Owicki-Gries-style proof cal…
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…
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…
Proof-Carrying Hardware via IC3
Tobias Isenberg, Heike Wehrheim
Proof-carrying hardware (PCH) is an approach to achieving safety of dynamically reconfigurable hardware, transferring the idea of proof-carrying code to the hardware domain. Curren…
A CSP Account of Event-B Refinement
Steve Schneider, Helen Treharne, Heike Wehrheim
Event-B provides a flexible framework for stepwise system development via refinement. The framework supports steps for (a) refining events (one-by-one), (b) splitting events (one-b…