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…