Verification Artifacts in Cooperative Verification: Survey and Unifying Component Framework
Dirk Beyer, Heike Wehrheim · Lecture notes in computer science · 2020
Abstract The goal ofcooperativeverification is to combine verification approaches in such a way that they work together to verify a system model. In particular, cooperative verifiersprovideexchangeable information (verification artifacts)toother verifiers orconsumesuch informationfromother verifiers with the goal of increasing the overall effectiveness and efficiency of the verification process. This paper first gives an overview over approaches for leveraging strengths of different techniques, algorithms, and tools in order to increase the power and abilities of the state of the art in software verification. To limit the scope, we restrict our overview to tools and approaches for automatic program analysis. Second, we specifically outline cooperative verification approaches and discuss their employed verification artifacts. Third, we formalize all artifacts in a uniform way, thereby fixing their semantics and providing verifiers with a precise meaning of the exchanged information.