Non-termination Witnesses and Their Validation
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F25%3A00141827" target="_blank" >RIV/00216224:14330/25:00141827 - isvavai.cz</a>
Result on the web
<a href="https://ieeexplore.ieee.org/document/11334721" target="_blank" >https://ieeexplore.ieee.org/document/11334721</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1109/ASE63991.2025.00164" target="_blank" >10.1109/ASE63991.2025.00164</a>
Alternative languages
Result language
angličtina
Original language name
Non-termination Witnesses and Their Validation
Original language description
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.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
<a href="/en/project/GA23-06506S" target="_blank" >GA23-06506S: Advanced Analysis and Verification for Advanced Software</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach<br>I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace
Others
Publication year
2025
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Automated Software Engineering, ASE 2025
ISBN
9798350357332
ISSN
1527-1366
e-ISSN
—
Number of pages
13
Pages from-to
1969-1981
Publisher name
IEEE
Place of publication
Los Alamitos (USA)
Event location
Seoul
Event date
Jan 1, 2025
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
001706323100156