Exchanging Verification Witnesses between Verifiers

Abstract

Standard verification tools provide a counterexample to witness a specifica- tion violation. Since a few years, such a witness can be validated by an independent validator using an exchangeable witness format. This way, information about the violation can be shared across verifiers and the user can use standard tools to visualize and explore witnesses. This technique is not yet established for the correctness case, where a program fulfills a specification. Even for simple programs, users often struggle to comprehend why a program is correct, and there is no way to independently check the verification result. We recently closed this gap by complementing our earlier work on violation witnesses with correctness witnesses. The overall goal to make proofs avail- able to engineers is probably as old as programming itself, and proof-carrying code was proposed two decades ago — our goal is to make it practical: We consider witnesses as first-class exchangeable objects, stored independently from the source code and checked independently from the verifier that produced them, respecting the principle of separation of concerns. At any time, the correctness witness can be used to recon- struct a correctness proof to establish trust. We extended two state-of-the-art verifiers, CPACHECKER and ULTIMATEAUTOMIZER, to produce and validate witnesses.