7 citations · 8 across the 4 of their papers we have counts for
5 papers · 1 filter
Context-Aware Separation Logic
Roland Meyer, Thomas Wies, Sebastian Wolff
Separation logic is often praised for its ability to closely mimic the locality of state updates when reasoning about them at the level of assertions. The prover only needs to conc…
Make flows small again: revisiting the flow framework
Roland Meyer, Thomas Wies, Sebastian Wolff
We present a new flow framework for separation logic reasoning about programs that manipulate general graphs. The framework overcomes problems in earlier developments: it is based…
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…
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…
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…