University of Cambridge > Talks.cam > Isaac Newton Institute Seminar Series > Cooperative Software Verification: Combination Approaches that Share Information

Cooperative Software Verification: Combination Approaches that Share Information

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2022 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity