Effect Summaries for Thread-Modular Analysis
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F17%3APU127284" target="_blank" >RIV/00216305:26230/17:PU127284 - isvavai.cz</a>
Result on the web
<a href="https://link.springer.com/chapter/10.1007%2F978-3-319-66706-5_9" target="_blank" >https://link.springer.com/chapter/10.1007%2F978-3-319-66706-5_9</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-319-66706-5_9" target="_blank" >10.1007/978-3-319-66706-5_9</a>
Alternative languages
Result language
angličtina
Original language name
Effect Summaries for Thread-Modular Analysis
Original language description
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.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
Result was created during the realization of more than one project. More information in the Projects tab.
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2017
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
SAS 2017: Static Analysis
ISBN
978-3-319-66706-5
ISSN
0302-9743
e-ISSN
—
Number of pages
23
Pages from-to
169-191
Publisher name
Springer International Publishing
Place of publication
Cham
Event location
New York City
Event date
Aug 30, 2017
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
000455332000009