Checking several requirements at once by CEGAR
At present static verifiers, which are based on Counterexample Guided Abstraction Refinement (CEGAR), can prove correctness of a program against a specified requirement, find its violation in a program and stop analysis or exhaust the given resources without producing any useful result. If we use this approach for checking several requirements at once, then finding a first violation of some requirement or exhausting resources for some requirement will prevent checking the program against other requirements. In particular we may miss violations of some requirements. That is why in practice each requirement to the program is usually checked separately. However, static verifiers perform similar actions during checking of the same program against different requirements and thus a lot of resources are wasted. This paper presents a new CEGAR-based method for software static verification, that is aimed at checking programs against several requirements at once and getting the same result as basic CEGAR, which checks requirements one by one. In order to do it the suggested method divides resources among requirements equally and continues analysis after finding violation of requirement excluding that requirement. We used Linux kernel modules to conduct experiments, in which implementation of the suggested method reduced total verification time by 5 times. The total number of divergent results in comparison with CEGAR was about 2 %.
Lecture Notes in Computer Science. — 2016. — Vol. 9609. — P. 218–232.