Proceedings of ISP RAS

Combination of static verification methods for checking requirements composition

V.O. Mordan (ISP RAS, Moscow, Russia)


Static verification proves correctness of the software against checked requirements, but it requires a lot of resources for that and its task is undecidable in general case. At present there is no universal static verification method, which could efficiently check any software. That is why one should choose more appropriate method and set its parameters for checking correctness of the given requirements in a given program. This paper suggests to combine different static verification methods in order to increase efficiency and effectiveness of verification, which is the first step in creating universal method for static verification. The suggested methods were implemented as combination of actively developing static verification methods for checking requirements composition. Implementation of the suggested methods showed their advantages on Linux kernel modules in comparison with using of each verification method separately.


software model checking; counterexample guided abstraction refinement; reachability task; requirements composition


Proceedings of the Institute for System Programming, vol. 29, issue 3, 2017, pp. 151-170.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2017-29(3)-9

Full text of the paper in pdf (in Russian) Back to the contents of the volume