Checking several requirements at once by CEGAR

Аннотация

Currently, static verifiers 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. Theoretically, we could use this approach for checking several requirements at once; however, finding of the first violation of some requirement or exhausting resources for some requirement will prevent from checking the program against other requirements. Moreover, if the program contains more than one violation of the requirement, CEGAR will find only the very first violation and may miss potential errors in the program. At the same time, static verifiers perform similar actions during checking of the same program against different requirements, which results in waste of a lot of resources. This paper presents a new CEGAR-based method for software static verification, which is aimed at checking programs against several requirements at once and getting the same result as basic CEGAR checking requirements one by one. To achieve this goal, the suggested method distributes resources over requirements and continues analysis after finding a violation of a requirement. We used Linux kernel modules to conduct experiments, in which implementation of the suggested method reduced total verification time by five times. The total number of divergent results in comparison with the base CEGAR was about 2%. Having continued the analysis after finding the first violation, this method guarantees that all violations of given requirements are found in 40% of cases, with the number of violations found being 1.5 times greater than in that in the base CEGAR approach.