7 citations · 8 across the 2 of their papers we have counts for
3 papers
cs.PL2019★ 7 cited
Pointer Life Cycle Types for Lock-Free Data Structures with Memory Reclamation
Roland Meyer, Sebastian Wolff
We consider the verification of lock-free data structures that manually manage their memory with the help of a safe memory reclamation (SMR) algorithm. Our first contribution is a…
cs.PL2018
Decoupling Lock-Free Data Structures from Memory Reclamation for Static Analysis
Roland Meyer, Sebastian Wolff
Verification of concurrent data structures is one of the most challenging tasks in software verification. The topic has received considerable attention over the course of the last…
cs.PL2017★ 1 cited
Effect Summaries for Thread-Modular Analysis
Lukáš Holík, Roland Meyer, Tomáš Vojnar +1
We propose a novel guess-and-check principle to increase the efficiency of thread-modular verification of lock-free data structures. We build on a heuristic that guesses candidates…