Lazy Abstractions for Size-Change Termination

Michael Codish, Carsten Fuhs, Jürgen Giesl, Peter Schneider-Kamp

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

Abstract

Size-change termination is a widely used means of proving termination where source programs are first abstracted to size-change graphs which are then analyzed to determine if they satisfy the size-change termination property. Here, the choice of the abstraction is crucial to the success of the method, and it is an open problem how to choose an abstraction such that no critical loss of precision occurs. This paper shows how to couple the search for a suitable abstraction and the test for size-change termination via an encoding to a single SAT instance. In this way, the problem of choosing the right abstraction is solved en passant by a SAT solver. We show that for the setting of term rewriting, the integration of this approach into the dependency pair framework works smoothly and gives rise to a new class of size-change reduction pairs. We implemented size-change reduction pairs in the termination prover AProVE and evaluated their usefulness in extensive experiments.
Original languageEnglish
Title of host publicationInternational Conference on Logic for Programming Artificial Intelligence and Reasoning
EditorsChristian G. Fermüller, Andrei Voronkov
PublisherSpringer
Publication date2010
Pages217-232
ISBN (Print)978-3-642-16241-1
ISBN (Electronic)978-3-642-16242-8
DOIs
Publication statusPublished - 2010
SeriesLecture Notes in Computer Science
Volume6397
ISSN0302-9743

Fingerprint

Experiments

Cite this

Codish, M., Fuhs, C., Giesl, J., & Schneider-Kamp, P. (2010). Lazy Abstractions for Size-Change Termination. In C. G. Fermüller, & A. Voronkov (Eds.), International Conference on Logic for Programming Artificial Intelligence and Reasoning (pp. 217-232). Springer. Lecture Notes in Computer Science, Vol.. 6397 https://doi.org/10.1007/978-3-642-16242-8_16
Codish, Michael ; Fuhs, Carsten ; Giesl, Jürgen ; Schneider-Kamp, Peter. / Lazy Abstractions for Size-Change Termination. International Conference on Logic for Programming Artificial Intelligence and Reasoning. editor / Christian G. Fermüller ; Andrei Voronkov. Springer, 2010. pp. 217-232 (Lecture Notes in Computer Science, Vol. 6397).
@inproceedings{2e9fae31f0b74c73a58a590e58dd9e36,
title = "Lazy Abstractions for Size-Change Termination",
abstract = "Size-change termination is a widely used means of proving termination where source programs are first abstracted to size-change graphs which are then analyzed to determine if they satisfy the size-change termination property. Here, the choice of the abstraction is crucial to the success of the method, and it is an open problem how to choose an abstraction such that no critical loss of precision occurs. This paper shows how to couple the search for a suitable abstraction and the test for size-change termination via an encoding to a single SAT instance. In this way, the problem of choosing the right abstraction is solved en passant by a SAT solver. We show that for the setting of term rewriting, the integration of this approach into the dependency pair framework works smoothly and gives rise to a new class of size-change reduction pairs. We implemented size-change reduction pairs in the termination prover AProVE and evaluated their usefulness in extensive experiments.",
author = "Michael Codish and Carsten Fuhs and J{\"u}rgen Giesl and Peter Schneider-Kamp",
note = "Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-17)",
year = "2010",
doi = "10.1007/978-3-642-16242-8_16",
language = "English",
isbn = "978-3-642-16241-1",
pages = "217--232",
editor = "Ferm{\"u}ller, {Christian G.} and Voronkov, {Andrei }",
booktitle = "International Conference on Logic for Programming Artificial Intelligence and Reasoning",
publisher = "Springer",
address = "Germany",

}

Codish, M, Fuhs, C, Giesl, J & Schneider-Kamp, P 2010, Lazy Abstractions for Size-Change Termination. in CG Fermüller & A Voronkov (eds), International Conference on Logic for Programming Artificial Intelligence and Reasoning. Springer, Lecture Notes in Computer Science, vol. 6397, pp. 217-232. https://doi.org/10.1007/978-3-642-16242-8_16

Lazy Abstractions for Size-Change Termination. / Codish, Michael; Fuhs, Carsten; Giesl, Jürgen; Schneider-Kamp, Peter.

International Conference on Logic for Programming Artificial Intelligence and Reasoning. ed. / Christian G. Fermüller; Andrei Voronkov. Springer, 2010. p. 217-232 (Lecture Notes in Computer Science, Vol. 6397).

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

TY - GEN

T1 - Lazy Abstractions for Size-Change Termination

AU - Codish, Michael

AU - Fuhs, Carsten

AU - Giesl, Jürgen

AU - Schneider-Kamp, Peter

N1 - Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-17)

PY - 2010

Y1 - 2010

N2 - Size-change termination is a widely used means of proving termination where source programs are first abstracted to size-change graphs which are then analyzed to determine if they satisfy the size-change termination property. Here, the choice of the abstraction is crucial to the success of the method, and it is an open problem how to choose an abstraction such that no critical loss of precision occurs. This paper shows how to couple the search for a suitable abstraction and the test for size-change termination via an encoding to a single SAT instance. In this way, the problem of choosing the right abstraction is solved en passant by a SAT solver. We show that for the setting of term rewriting, the integration of this approach into the dependency pair framework works smoothly and gives rise to a new class of size-change reduction pairs. We implemented size-change reduction pairs in the termination prover AProVE and evaluated their usefulness in extensive experiments.

AB - Size-change termination is a widely used means of proving termination where source programs are first abstracted to size-change graphs which are then analyzed to determine if they satisfy the size-change termination property. Here, the choice of the abstraction is crucial to the success of the method, and it is an open problem how to choose an abstraction such that no critical loss of precision occurs. This paper shows how to couple the search for a suitable abstraction and the test for size-change termination via an encoding to a single SAT instance. In this way, the problem of choosing the right abstraction is solved en passant by a SAT solver. We show that for the setting of term rewriting, the integration of this approach into the dependency pair framework works smoothly and gives rise to a new class of size-change reduction pairs. We implemented size-change reduction pairs in the termination prover AProVE and evaluated their usefulness in extensive experiments.

U2 - 10.1007/978-3-642-16242-8_16

DO - 10.1007/978-3-642-16242-8_16

M3 - Article in proceedings

SN - 978-3-642-16241-1

SP - 217

EP - 232

BT - International Conference on Logic for Programming Artificial Intelligence and Reasoning

A2 - Fermüller, Christian G.

A2 - Voronkov, Andrei

PB - Springer

ER -

Codish M, Fuhs C, Giesl J, Schneider-Kamp P. Lazy Abstractions for Size-Change Termination. In Fermüller CG, Voronkov A, editors, International Conference on Logic for Programming Artificial Intelligence and Reasoning. Springer. 2010. p. 217-232. (Lecture Notes in Computer Science, Vol. 6397). https://doi.org/10.1007/978-3-642-16242-8_16