Combination of static verification methods for checking requirements composition (in Russian)

Static verification proves the correctness of software with respect to specified requirements; however, it requires substantial computational resources, and the verification problem is undecidable in the general case. At present, there is no universal static verification method that can efficiently check arbitrary software. Therefore, it is necessary to select an appropriate verification method and configure its parameters to check the correctness of given requirements in a particular program.

This paper proposes combining different static verification methods in order to improve both the efficiency and effectiveness of verification, which is a step toward the development of a universal static verification approach. The proposed methods were implemented as a combination of actively developed static verification techniques for checking requirements composition. Experimental evaluation on Linux kernel modules demonstrates the advantages of the proposed approach compared to using each verification method separately.