Non-termination Witnesses and Their Validation

D 2025

Non-termination Witnesses and Their Validation

ÁDÁM, Zsófia; Paulína AYAZIOVÁ; Levente BAJCZI; Dirk BEYER; Marek JANKOLA et al.

Základní údaje

Originální název

Non-termination Witnesses and Their Validation

Autoři

ÁDÁM, Zsófia; Paulína AYAZIOVÁ; Levente BAJCZI; Dirk BEYER; Marek JANKOLA; Marian LINGSCH-ROSENFELD a Jan STREJČEK

Vydání

Los Alamitos (USA), Automated Software Engineering, ASE 2025, od s. 1969-1981, 13 s. 2025

Nakladatel

IEEE

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

elektronická verze "online"

Odkazy

URL

Označené pro přenos do RIV

Ano

Organizační jednotka

Fakulta informatiky

ISBN

979-8-3503-5733-2

DOI

https://doi.org/10.1109/ASE63991.2025.00164

Klíčová slova anglicky

verification witness; software verification; validation; exchange format; invariant; counterexample

Štítky

AVELAB, core_A, firank_1, program analysis, verification, verification witnesses

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 19. 3. 2026 19:10, prof. RNDr. Jan Strejček, Ph.D.

Anotace

V originále

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.

Návaznosti

GA23-06506S, projekt VaV

Název: Pokročilá analýza a verifikace pro pokročilý software

Investor: Grantová agentura ČR, Pokročilá analýza a verifikace pro pokročilý software

MUNI/A/1666/2024, interní kód MU

Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 25

Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 25

Citovat

ÁDÁM, Zsófia; Paulína AYAZIOVÁ; Levente BAJCZI; Dirk BEYER; Marek JANKOLA; Marian LINGSCH-ROSENFELD a Jan STREJČEK. Non-termination Witnesses and Their Validation. Online. In Automated Software Engineering, ASE 2025. Los Alamitos (USA): IEEE, 2025, s. 1969-1981. ISBN 979-8-3503-5733-2. Dostupné z: https://doi.org/10.1109/ASE63991.2025.00164.

@inproceedings{2513857,
   author = {Ádám, Zsófia and Ayaziová, Paulína and Bajczi, Levente and Beyer, Dirk and Jankola, Marek and LingschandRosenfeld, Marian and Strejček, Jan},
   address = {Los Alamitos (USA)},
   booktitle = {Automated Software Engineering, ASE 2025},
   doi = {https://doi.org/10.1109/ASE63991.2025.00164},
   keywords = {verification witness; software verification; validation; exchange format; invariant; counterexample},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Los Alamitos (USA)},
   isbn = {979-8-3503-5733-2},
   pages = {1969-1981},
   publisher = {IEEE},
   title = {Non-termination Witnesses and Their Validation},
   url = {https://ieeexplore.ieee.org/document/11334721},
   year = {2025}
}

TY  - CONF
ID  - 2513857
AU  - Ádám, Zsófia - Ayaziová, Paulína - Bajczi, Levente - Beyer, Dirk - Jankola, Marek - Lingsch-Rosenfeld, Marian - Strejček, Jan
PY  - 2025
TI  - Non-termination Witnesses and Their Validation
PB  - IEEE
CY  - Los Alamitos (USA)
SN  - 9798350357332
KW  - verification witness
KW  - software verification
KW  - validation
KW  - exchange format
KW  - invariant
KW  - counterexample
UR  - https://ieeexplore.ieee.org/document/11334721
N2  - 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.
ER  -

ÁDÁM, Zsófia; Paulína AYAZIOVÁ; Levente BAJCZI; Dirk BEYER; Marek JANKOLA; Marian LINGSCH-ROSENFELD a Jan STREJČEK. Non-termination Witnesses and Their Validation. Online. In \textit{Automated Software Engineering, ASE 2025}. Los Alamitos (USA): IEEE, 2025, s.~1969-1981. ISBN~979-8-3503-5733-2. Dostupné z: https://doi.org/10.1109/ASE63991.2025.00164.

Přehled o publikaci