Home > Verimag > Seminars

Seminar details

IMAG 206
30 March 2017 - 10h00
Correctness Witnesses: Exchanging Verification Results between Verifiers
by Dirk Beyer from Ludwig-Maximilians-Universitaet Muenchen

Abstract: Standard verification tools provide a counterexample to witness a specification violation,
and, 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 verification tools
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, it is often difficult for users to comprehend why a given program is correct,
and there is no way to independently check the verification result.
We close this gap by complementing our earlier work on violation witnesses
with correctness witnesses.
While we use an extension of the established common exchange format for violation witnesses
to represent correctness witnesses,
the techniques for producing and validating correctness witnesses are different.
The overall goal to make proofs available 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 important principle of separation of concerns.
At any time, the invariants from the correctness witness can be used to reconstruct a correctness proof to establish trust.
We extended two state-of-the-art verifiers, CPAchecker and Ultimate Automizer, to produce and validate witnesses, and report that the approach is promising on a large set of verification tasks.

Slides of the Presentation.