Abstract 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.

Major breakthroughs have increased the efficiency and effectiveness of software model checking considerably, such that this technology is now applicable to industrial-scale software. However, verifying the full formal specification of a software system is still considered too complex, and in practice, sets of properties are verified one by one in isolation. We propose an approach that takes the full formal specification as input and first tries to verify all properties simultaneously in one verification run. Our verification algorithm monitors itself and detects situations for which the full set of properties is too complex. In such cases, we perform an automatic decomposition of the full set of properties into smaller sets, and continue the verification seamlessly. To avoid state-space explosion for large sets of properties, we introduce on-the-fly property weaving: properties get weaved into the program's transition system on the fly, during the analysis; which properties to weave and verify is determined dynamically during the verification process. We perform an extensive evaluation based on verification tasks that were derived from 4336 Linux kernel modules, and a set of properties that define the correct usage of the Linux API. Checking several properties simultaneously can lead to a significant performance gain, due to the fact that abstract models share many parts among different properties.

Concurrent systems work nondeterministically. For concurrent systems, UniTESK-based test suite executes methods with different parameters in different states, but it does not guarantee that all possible execution paths of a method will be tested because of its concurrent nature. This paper presents an integration method that combines the testing techniques with model checking techniques of Java PathFinder (JPF). The method guarantees that all possible execution paths needed for checking the correctness of the system are explored. The method is based on localization of the search performed by JPF. It reduces the state space while preserving the advantages of UniTESK like state abstraction and automatic checking of correctness. Moreover, it allows to use the same test suite without modification with JPF.