A lightweight approach to nontermination inference using Constrained Horn Clauses

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

doi:10.1007/s10270-024-01161-5

A lightweight approach to nontermination inference using Constrained Horn Clauses

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

Department of Data Science & AI

Research output: Contribution to journal › Article › Research › peer-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 language	English
Pages (from-to)	319–342
Number of pages	24
Journal	Software and Systems Modeling
Volume	23
DOIs	https://doi.org/10.1007/s10270-024-01161-5
Publication status	Published - Apr 2024

Keywords

Abstract interpretation
Constrained Horn clauses
Nontermination
Precondition inference
Program transformation

Access to Document

10.1007/s10270-024-01161-5

Cite this

@article{902355bcd9614b99a71a60da7676ab41,

title = "A lightweight approach to nontermination inference using Constrained Horn Clauses",

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.",

keywords = "Abstract interpretation, Constrained Horn clauses, Nontermination, Precondition inference, Program transformation",

author = "Bishoksan Kafle and Graeme Gange and Peter Schachte and Harald S{\o}ndergaard and Stuckey, {Peter J.}",

note = "Funding Information: We thank John Gallagher and the anonymous reviewers for their insightful comments, which led to many improvements. Bishoksan Kafle has been partially funded by the Spanish Ministry of Research, Science and Innovation, grant MICINN PID2019-108528RB-C21 ProCode and Madrid P2018/TCS-4339 BLOQUES-CM. Peter Stuckey{\textquoteright}s work was supported by the Australian Research Council OPTIMA ITTC, Project ID IC200100009. Publisher Copyright: {\textcopyright} The Author(s), under exclusive licence to Springer-Verlag GmbH Germany, part of Springer Nature 2024.",

year = "2024",

month = apr,

doi = "10.1007/s10270-024-01161-5",

language = "English",

volume = "23",

pages = "319–342",

journal = "Software and Systems Modeling",

issn = "1619-1366",

publisher = "Springer",

}

TY - JOUR

T1 - A lightweight approach to nontermination inference using Constrained Horn Clauses

AU - Kafle, Bishoksan

AU - Gange, Graeme

AU - Schachte, Peter

AU - Søndergaard, Harald

AU - Stuckey, Peter J.

N1 - Funding Information: We thank John Gallagher and the anonymous reviewers for their insightful comments, which led to many improvements. Bishoksan Kafle has been partially funded by the Spanish Ministry of Research, Science and Innovation, grant MICINN PID2019-108528RB-C21 ProCode and Madrid P2018/TCS-4339 BLOQUES-CM. Peter Stuckey’s work was supported by the Australian Research Council OPTIMA ITTC, Project ID IC200100009. Publisher Copyright: © The Author(s), under exclusive licence to Springer-Verlag GmbH Germany, part of Springer Nature 2024.

PY - 2024/4

Y1 - 2024/4

N2 - 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.

AB - 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.

KW - Abstract interpretation

KW - Constrained Horn clauses

KW - Nontermination

KW - Precondition inference

KW - Program transformation

UR - http://www.scopus.com/inward/record.url?scp=85187867291&partnerID=8YFLogxK

U2 - 10.1007/s10270-024-01161-5

DO - 10.1007/s10270-024-01161-5

M3 - Article

AN - SCOPUS:85187867291

SN - 1619-1366

VL - 23

SP - 319

EP - 342

JO - Software and Systems Modeling

JF - Software and Systems Modeling

ER -

A lightweight approach to nontermination inference using Constrained Horn Clauses

Abstract

Keywords

Access to Document

Other files and links

ARC Training Centre in Optimisation Technologies, Integrated Methodologies, and Applications (OPTIMA)

Cite this

A lightweight approach to nontermination inference using Constrained Horn Clauses

Abstract

Keywords

Access to Document

Other files and links

Projects

ARC Training Centre in Optimisation Technologies, Integrated Methodologies, and Applications (OPTIMA)

Cite this