Verification Witnesses Version 2
This work is accepted at an awsome conference.
A 
preprint
and the 
publisher's version
of this article are available for you to download.
Abstract
Verification witnesses are now widely accepted objects used not only to confirm or refute verification results, but also for general exchange of information among various program verification tools. The original format for witnesses is based on GraphML and it has some known issues including unclear semantics, limited support of some parts, and large witness files. This paper presents a new witness format based on YAML that aims to remove the mentioned issues. We also describe the current tool support of the format and provide an experimental comparison of various aspects of the original and the new witness format.
Tool and Reproduction Information
A reproduction package of this work is available on Zenodo
(
).
Full Results
The experimental results reported in the paper can be seen in the interactive tables below. You can click on the cells in the status columns to see the corresponding log output and use the respective tabs to show various plots.
- Coming Soon