Lightweight nontermination inference with CHCs

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

doi:10.1007/978-3-030-92124-8_22

Lightweight nontermination inference with CHCs

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

Department of Data Science & AI

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › Research

1 Citation (Scopus)

Abstract

Non-termination is an unwanted program property (considered a bug) for some software systems, and a safety property for other systems. In either case, automated discovery of preconditions for non-termination is of interest. We introduce NtHorn, a fast lightweight non-termination analyser, able to deduce non-trivial sufficient conditions for non-termination. 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 non-termination analysis. NtHorn is comparable in power to the state-of-the-art non-termination analysis tools, as measured on standard competition benchmark suites (consisting of integer manipulating programs), while typically solving problems an order of magnitude faster.

Original language	English
Title of host publication	19th International Conference, SEFM 2021 Virtual Event, December 6–10, 2021 Proceedings
Editors	Radu Calinescu, Corina S. Pasareanu
Place of Publication	Cham Switzerland
Publisher	Springer
Pages	383-402
Number of pages	20
ISBN (Electronic)	9783030921248
ISBN (Print)	9783030921231
DOIs	https://doi.org/10.1007/978-3-030-92124-8_22
Publication status	Published - 2021
Event	International Conference on Software Engineering and Formal Methods 2021 - Online, Switzerland Duration: 6 Dec 2021 → 10 Dec 2021 Conference number: 19th https://link.springer.com/book/10.1007/978-3-030-92124-8 (Proceedings)

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	13085
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	International Conference on Software Engineering and Formal Methods 2021
Abbreviated title	SEFM 2021
Country/Territory	Switzerland
Period	6/12/21 → 10/12/21
Internet address	https://link.springer.com/book/10.1007/978-3-030-92124-8 (Proceedings)

Access to Document

10.1007/978-3-030-92124-8_22

Cite this

Kafle, B., Gange, G., Schachte, P., Søndergaard, H., & Stuckey, P. J. (2021). Lightweight nontermination inference with CHCs. In R. Calinescu, & C. S. Pasareanu (Eds.), 19th International Conference, SEFM 2021 Virtual Event, December 6–10, 2021 Proceedings (pp. 383-402). (Lecture Notes in Computer Science; Vol. 13085). Springer. https://doi.org/10.1007/978-3-030-92124-8_22

@inproceedings{683030d388eb4ba3854cebfe4bd82ecd,

title = "Lightweight nontermination inference with CHCs",

abstract = "Non-termination is an unwanted program property (considered a bug) for some software systems, and a safety property for other systems. In either case, automated discovery of preconditions for non-termination is of interest. We introduce NtHorn, a fast lightweight non-termination analyser, able to deduce non-trivial sufficient conditions for non-termination. 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 non-termination analysis. NtHorn is comparable in power to the state-of-the-art non-termination analysis tools, as measured on standard competition benchmark suites (consisting of integer manipulating programs), while typically solving problems an order of magnitude faster.",

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

note = "Funding Information: Acknowledgements. We thank the three anonymous reviewers for their careful reading of an earlier version of the paper, and their constructive suggestions for how to improve it. 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. Publisher Copyright: {\textcopyright} 2021, Springer Nature Switzerland AG.; International Conference on Software Engineering and Formal Methods 2021, SEFM 2021 ; Conference date: 06-12-2021 Through 10-12-2021",

year = "2021",

doi = "10.1007/978-3-030-92124-8_22",

language = "English",

isbn = "9783030921231",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "383--402",

editor = "Radu Calinescu and Pasareanu, {Corina S.}",

booktitle = "19th International Conference, SEFM 2021 Virtual Event, December 6–10, 2021 Proceedings",

url = "https://link.springer.com/book/10.1007/978-3-030-92124-8",

}

Kafle, B, Gange, G, Schachte, P, Søndergaard, H & Stuckey, PJ 2021, Lightweight nontermination inference with CHCs. in R Calinescu & CS Pasareanu (eds), 19th International Conference, SEFM 2021 Virtual Event, December 6–10, 2021 Proceedings. Lecture Notes in Computer Science, vol. 13085, Springer, Cham Switzerland, pp. 383-402, International Conference on Software Engineering and Formal Methods 2021, Switzerland, 6/12/21. https://doi.org/10.1007/978-3-030-92124-8_22

Lightweight nontermination inference with CHCs. / Kafle, Bishoksan; Gange, Graeme; Schachte, Peter et al.
19th International Conference, SEFM 2021 Virtual Event, December 6–10, 2021 Proceedings. ed. / Radu Calinescu; Corina S. Pasareanu. Cham Switzerland: Springer, 2021. p. 383-402 (Lecture Notes in Computer Science; Vol. 13085).

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › Research

TY - GEN

T1 - Lightweight nontermination inference with CHCs

AU - Kafle, Bishoksan

AU - Gange, Graeme

AU - Schachte, Peter

AU - Søndergaard, Harald

AU - Stuckey, Peter J.

N1 - Conference code: 19th

PY - 2021

Y1 - 2021

N2 - Non-termination is an unwanted program property (considered a bug) for some software systems, and a safety property for other systems. In either case, automated discovery of preconditions for non-termination is of interest. We introduce NtHorn, a fast lightweight non-termination analyser, able to deduce non-trivial sufficient conditions for non-termination. 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 non-termination analysis. NtHorn is comparable in power to the state-of-the-art non-termination analysis tools, as measured on standard competition benchmark suites (consisting of integer manipulating programs), while typically solving problems an order of magnitude faster.

AB - Non-termination is an unwanted program property (considered a bug) for some software systems, and a safety property for other systems. In either case, automated discovery of preconditions for non-termination is of interest. We introduce NtHorn, a fast lightweight non-termination analyser, able to deduce non-trivial sufficient conditions for non-termination. 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 non-termination analysis. NtHorn is comparable in power to the state-of-the-art non-termination analysis tools, as measured on standard competition benchmark suites (consisting of integer manipulating programs), while typically solving problems an order of magnitude faster.

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

U2 - 10.1007/978-3-030-92124-8_22

DO - 10.1007/978-3-030-92124-8_22

M3 - Conference Paper

AN - SCOPUS:85121928193

SN - 9783030921231

T3 - Lecture Notes in Computer Science

SP - 383

EP - 402

BT - 19th International Conference, SEFM 2021 Virtual Event, December 6–10, 2021 Proceedings

A2 - Calinescu, Radu

A2 - Pasareanu, Corina S.

PB - Springer

CY - Cham Switzerland

T2 - International Conference on Software Engineering and Formal Methods 2021

Y2 - 6 December 2021 through 10 December 2021