Abstract

Cooperative verification is an approach where several verifiers help each other solving the verification problem by sharing artifacts about the verification task. There are many verification tools available, but the power of combining them is not yet fully leveraged. The probem is that in order to use verifiers ‘off-the-shelf’, we need clear interfaces to invoke the tools and to pass information. Part of the interfacing probem is to define standard artifacts to be passed between verifiers. We first give a brief overview of CPAchecker, an open-source framework for software verification, and then explain a few recent approaches for cooperative combinations. PDF of presentation: https://www.sosy-lab.org/research/prs/2022-07-07_VVS22_CooperativeVerification_Dirk.pdf References:

Verification Witnesses (TOSEM): https://doi.org/10.1145/3477579 A Unifying View on SMT -Based Software Verification (JAR): https://doi.org/10.1007/s10817-017-9432-6 CoVeriTeam: On-Demand Composition of Cooperative Verification Systems (Proc. TACAS ): https://doi.org/10.1007/978-3-030-99524-9_31 Decomposing Software Verification into Off-the-Shelf Components: An Application to CEGAR (Proc. ICSE ): https://www.sosy-lab.org/research/pub/2022-ICSE.Decomposing_Software_Verification_into_Off-the-Shelf-Components.pdf