cpalockator: Thread-Modular Analysis with Projections: (Competition Contribution)

Our submission to SV-COMP’21 is based on the software verification framework [Image: see text] 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: see text] framework allows combining our approach with existing algorithms and analyses. Evaluation on the sv-benchmarks confirms the scalability and soundness of the approach.