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.
