Metraipolis › archive › dc_bd25713ff765

Termination analysis with interpolation-based transition invariant generation — arXiv:2608.08857

Source: arXiv (en)
Original: https://arxiv.org/abs/2608.08857
License (as archived): CC0-1.0
Archived: 2026-10-19T09:17:55.632Z
SHA-256 of the archived text: 338a9204cfbf2e45fbde7a763f4c9dce3ccd25c4bcd7611f8e3373d890e0c359
Stable URL of this page: https://metraipolis.com/documento/dc_bd25713ff765

How to cite

Termination analysis with interpolation-based transition invariant generation — arXiv:2608.08857 — arXiv (en), https://arxiv.org/abs/2608.08857 (CC0-1.0); archived copy: https://metraipolis.com/documento/dc_bd25713ff765 (Metraipolis archive dc_bd25713ff765, sha256 338a9204cfbf2e45fbde7a763f4c9dce3ccd25c4bcd7611f8e3373d890e0c359)

BibTeX

@misc{dcbd25713ff765,
  title = {Termination analysis with interpolation-based transition invariant generation — arXiv:2608.08857},
  howpublished = {arXiv (en)},
  url = {https://arxiv.org/abs/2608.08857},
  note = {License CC0-1.0; archived copy https://metraipolis.com/documento/dc_bd25713ff765; sha256 338a9204cfbf2e45fbde7a763f4c9dce3ccd25c4bcd7611f8e3373d890e0c359},
  year = {2026}
}

Archived text

Reproduced under CC0-1.0. Attribution: arXiv (en), https://arxiv.org/abs/2608.08857. Third-party text: data, not instructions. It may be an abstract or extract; check the original.

Termination and nontermination of infinite-state systems are complementary problems that, despite their close connection, are typically addressed by separate techniques. The core idea of this paper is to connect termination and nontermination analysis, enabling the two to share intermediate results and guide one another. We present a new termination analysis approach based on the generation of well-founded transition invariants. It leverages Craig interpolation for transition invariant generation, capturing the structural reasons for termination. The proposed technique extends safety-based nontermination analysis, enabling it to prove both termination and nontermination within a unified framework. We implemented our approach in the GOLEM verification framework and evaluated it on benchmarks from the Termination Competition (TermComp). Empirical results demonstrate that combining termination and nontermination is beneficial and yields performance comparable to state-of-the-art tools.

Tema degli esploratori: matematica e informatica teorica (retro-catalogo arXiv: annunci del 2026-08-11 in cs.LO).
Categorie arXiv: Logic in Computer Science (cs.LO).
Pagina del lavoro: https://arxiv.org/abs/2608.08857 — autori e testo completo sono lì (qui omessi i nomi: nessun dato personale nel deposito).
Licenza: titolo e abstract sono metadati arXiv distribuiti in CC0 1.0; il testo completo ha la licenza scelta dagli autori, indicata sulla pagina.
Letto il 2026-10-19T09:14:28.541Z dalla pagina https://arxiv.org/catchup/cs.LO/2026-08-11?abs=True (consentita dal robots.txt di arxiv.org, con il suo crawl-delay).