Cooperative Software Verification: Combination Approaches that Share Information

Add to your list(s) Download to your calendar using vCal

• Dirk Beyer (Ludwig-Maximilians-Universität München)
• Thursday 07 July 2022, 09:30-10:30
• Seminar Room 1, Newton Institute.

If you have a question about this talk, please contact nobody.

VS2W01 - Vistas in Verified Software

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

This talk is part of the Isaac Newton Institute Seminar Series series.

This talk is included in these lists:

• All CMS events
• Featured lists
• INI info aggregator
• Isaac Newton Institute Seminar Series
• School of Physical Sciences
• Seminar Room 1, Newton Institute
• bld31

Note that ex-directory lists are not shown.