Non-termination Witnesses and Their Validation
preprintAbstract
Designing algorithms for complex problems as certifying algorithms is an important approach to ensure correctness of computational results. Instead of producing an output y for an input x, a certifying algorithm produces as output for x not only y but also a witness w. The witness w (also called certificate) can now be used to check that y is indeed the correct output for input x. Witnesses and their validation also exist in the area of automatic software verification, and a large number of tools support verification witnesses. SV-COMP 2025 reports 62 verifiers producing witnesses and 18 tools for witness validation. In 2023, a new version 2.0 of the witness format for software verification was introduced to overcome several problems with the previous format, and this new format is now widely supported. However, there is no format with a clear definition and semantics for witnesses of non-termination. This paper closes this gap by presenting an extension of the witness format 2.0 to support program non-termination. Besides explaining the design of this extension, we describe various approaches to generate and validate non-termination witnesses. We also give an overview of current tool support of the extended format, i.e., the verifiers that can generate non-termination witnesses and the witness validators able to analyze these witnesses. Finally, we present an experimental evaluation showing the performance of these tools on program-termination tasks of SV-COMP 2025.
Reproduction Information
Our reproduction package, which includes all software and data that we used for our experiments, and the set of example witnesses to demonstrate how the new format works, are available on Zenodo.
Experimental Results
The experimental results reported in the paper can be viewed in the interactive tables linked below. You can click on the cells in the status columns to see the respective log output and navigate through the tabs to view various plots.
The following list contains, for each of the 6 producers of witnesses, a table that shows the results for validating the witnesses.
The following list contains restricted views of the above tables, for each of the 6 producers of witnesses, a row that corresponds to a column in Table II of the paper.
The following list contains scatter plots in the same interactive framework as the above tables. They contain every combination of verifier-validator in a separate scatter plot. We do not include TransVer based tools as the naming for the unreach-call tasks do not match the termination tasks in the tables.
| Verifier | Validator 1 | Validator 2 | Validator 3 | Validator 4 | Validator 5 | Validator 6 |
|---|---|---|---|---|---|---|
| EmergenTheta | CPAchecker | Witch | Theta | EmergenTheta | Thorn | Theta-modular |
| Symbiotic | CPAchecker | Witch | Theta | EmergenTheta | Thorn | Theta-modular |
| Theta | CPAchecker | Witch | Theta | EmergenTheta | Thorn | Theta-modular |
| Thorn | CPAchecker | Witch | Theta | EmergenTheta | Thorn | Theta-modular |