A lightweight approach to nontermination inference using Constrained Horn Clauses

Bishoksan Kafle, Graeme Gange, Peter Schachte, Harald Søndergaard, Peter J. Stuckey

Research output: Contribution to journalArticleResearchpeer-review

Abstract

Nontermination is an unwanted program property for some software systems, and a safety property for other systems. In either case, automated discovery of preconditions for nontermination is of interest. We introduce NtHorn, a fast lightweight nontermination analyser, which is able to deduce non-trivial sufficient conditions for nontermination. Using Constrained Horn Clauses (CHCs) as a vehicle, we show how established techniques for CHC program transformation and abstract interpretation can be exploited for the purpose of nontermination analysis. NtHorn is comparable in effectiveness to the state-of-the-art nontermination analysis tools, as measured on standard competition benchmark suites (consisting of integer manipulating programs), while typically solving problems faster by one order of magnitude.

Original languageEnglish
Pages (from-to)319–342
Number of pages24
JournalSoftware and Systems Modeling
Volume23
DOIs
Publication statusPublished - Apr 2024

Keywords

  • Abstract interpretation
  • Constrained Horn clauses
  • Nontermination
  • Precondition inference
  • Program transformation

Cite this