CoVEGI: Cooperative Verification via Externally Generated Invariants

Abstract

Software verification has recently made enormous progress. To keep their tools up to date with novel methods and enhanced techniques, tool developers integrate these within their own framework almost exclusively by re-implementation. While this allows for a conceptual re-use of methods, it nevertheless requires novel implementations. Our configurable framework named CoVEGI employs cooperative verification in order to avoid re-implementation and enable usage of novel tools as black-box components in verification. Specifically, cooperation is employed for invariant generation, which is key to the success of a verification run. CoVEGI allows a main verification tool to delegate the task of invariant generation to one or several specialized helper invariant generators, utilizing their results within its verification run. The experimental evaluation shows that the use of CoVEGI can increase the number of correctly verified tasks up to 17%, without increasing the used resources.