cpalockator: Thread-Modular Analysis with Projections

Autor:	Pavel Andrianov, Vadim Mutilin, Alexey Khoroshilov
Rok vydání:	2021
Předmět:	Projection (mathematics) Computer science business.industry Multithreading Synchronization (computer science) Window (computing) Thread (computing) Parallel computing Modular design business Software verification Image (mathematics)
Zdroj:	Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783030720124 TACAS (2)
DOI:	10.1007/978-3-030-72013-1_25
Popis:	Our submission to SV-COMP’21 is based on the software verification framework "Image missing" and implements the extension to the thread-modular approach. It considers every thread separately, but in a special environment which models thread interactions. The environment is expressed by projections of normal transitions in each thread. A projection contains a description of possible effects over shared data and synchronization primitives, as well as conditions of its application. Adjusting the precision of the projections, one can find a balance between the speed and the precision of the whole analysis.Implementation on the top of the "Image missing" framework allows combining our approach with existing algorithms and analyses. Evaluation on the sv-benchmarks confirms the scalability and soundness of the approach.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::e093d963f150c2039020e06a1c9624ff https://doi.org/10.1007/978-3-030-72013-1_25 Zobrazit plný text záznamu