Presenter
Marek Jankola
LMU Munich
Authors
Dirk Beyer, Marek Jankola, and Marian Lingsch-Rosenfeld
Abstract
Whenever automated provers such as automatic software verifiers deliver a verdict (true or false), they are expected to produce also a witness that justifies the verdict. This allows independent validation of the verdict using the witness by a third party, increasing trust in the results. The current standard exchange formats for witnesses in software verification do not support program termination. To fill this gap, we propose an extension of the witness format that is based on transition invariants as a general and effective formalism. We justify this by (a) proving that transition invariants can encode other popular termination arguments like ranking functions and (b) providing three different validation approaches for transition invariants, which together can validate most of the exported witnesses. Our approach based on transition invariants was integrated into version 2.1 of the recently released witness format, and the software-verification community has adopted the format for SV-COMP.
Slides
TBA