Gastvortrag "Correctness Witnesses: Exchanging Verification Results between Verifiers" von Prof. Dirk Beyer

Am 18.05.2017 hält Prof. Dirk Beyer von der LMU ab 17:15 Uhr einen Gastvortrag in der Ringvorlesung des Elitestudiengangs Software Engineering. Das Thema lautet "Correctness Witnesses: Exchanging Verification Results between Verifiers". Der Vortrag findet in Raum 1057N statt. Alle sind herzlich eingeladen.


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.

Meldung vom 15.05.2017