Conference paper

HOLÍK Lukáš, MEYER Roland, VOJNAR Tomáš and WOLF Sebastian. Effect Summaries for Thread-Modular Analysis. In: SAS 2017: Static Analysis. Cham: Springer International Publishing, 2017, pp. 169-191. ISBN 978-3-319-66706-5. Available from:
Publication language:english
Original title:Effect Summaries for Thread-Modular Analysis
Title (cs):Souhrny efektů pro vláknově modulární analýzu
Proceedings:SAS 2017: Static Analysis
Conference:24th International Static Analysis Symposium
Series:Lecture Notes in Computer Science 10422
Place:Cham, DE
Publisher:Springer International Publishing
Concurrent programs, thread-modular reasoning, effect summary, unbounded concurrency, dynamic lockless data structures.
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 for stateless effect summaries of programs by searching the code for instances of a copy-and-check programming idiom common in lock-free data structures. These candidate summaries are used to compute the interference among threads in linear time. Since a candidate summary need not be a sound effect summary, we show how to fully automatically check whether the precision of candidate summaries is sufficient. We can thus perform sound verification despite relying on an unsound heuristic. We have implemented our approach and found it up to two orders of magnitude faster than existing ones.
   author = {Luk{\'{a}}{\v{s}} Hol{\'{i}}k and Roland Meyer and
	Tom{\'{a}}{\v{s}} Vojnar and Sebastian Wolf},
   title = {Effect Summaries for Thread-Modular Analysis},
   pages = {169--191},
   booktitle = {SAS 2017: Static Analysis},
   series = {Lecture Notes in Computer Science 10422},
   year = 2017,
   location = {Cham, DE},
   publisher = {Springer International Publishing},
   ISBN = {978-3-319-66706-5},
   doi = {10.1007/978-3-319-66706-5_9},
   language = {english},
   url = {}

Your IPv4 address:
Switch to https