33 citations · 37 across the 3 of their papers we have counts for
4 papers
Proving Linearizability Using Partial Orders (Extended Version)
Artem Khyzha, Mike Dodds, Alexey Gotsman +1
Linearizability is the commonly accepted notion of correctness for concurrent data structures. It requires that any execution of the data structure is justified by a linearization…
A Generic Logic for Proving Linearizability (Extended Version)
Artem Khyzha, Alexey Gotsman, Matthew Parkinson
Linearizability is a commonly accepted notion of correctness for libraries of concurrent algorithms, and recent years have seen a number of proposals of program logics for proving…
New Lace and Arsenic: adventures in weak memory with a program logic
Richard Bornat, Jade Alglave, Matthew Parkinson
We describe a program logic for weak memory (also known as relaxed memory). The logic is based on Hoare logic within a thread, and rely/guarantee between threads. It is presented v…
The Relationship Between Separation Logic and Implicit Dynamic Frames
Matthew J. Parkinson, Alexander J. Summers
Separation logic is a concise method for specifying programs that manipulate dynamically allocated storage. Partially inspired by separation logic, Implicit Dynamic Frames has rece…