Lazy Abstractions for Size-Change Termination

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

Publikation: Bidrag til bog/antologi/rapport/konference-proceedingKonferencebidrag i proceedingsForskningpeer review

Resumé

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.
OriginalsprogEngelsk
TitelInternational Conference on Logic for Programming Artificial Intelligence and Reasoning
RedaktørerChristian G. Fermüller, Andrei Voronkov
ForlagSpringer
Publikationsdato2010
Sider217-232
ISBN (Trykt)978-3-642-16241-1
ISBN (Elektronisk)978-3-642-16242-8
DOI
StatusUdgivet - 2010
NavnLecture Notes in Computer Science
Vol/bind6397
ISSN0302-9743

Fingeraftryk

Experiments

Citer dette

Codish, M., Fuhs, C., Giesl, J., & Schneider-Kamp, P. (2010). Lazy Abstractions for Size-Change Termination. I C. G. Fermüller, & A. Voronkov (red.), International Conference on Logic for Programming Artificial Intelligence and Reasoning (s. 217-232). Springer. Lecture Notes in Computer Science, Bind. 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. red. / Christian G. Fermüller ; Andrei Voronkov. Springer, 2010. s. 217-232 (Lecture Notes in Computer Science, Bind 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. i CG Fermüller & A Voronkov (red), International Conference on Logic for Programming Artificial Intelligence and Reasoning. Springer, Lecture Notes in Computer Science, bind 6397, s. 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. red. / Christian G. Fermüller; Andrei Voronkov. Springer, 2010. s. 217-232 (Lecture Notes in Computer Science, Bind 6397).

Publikation: Bidrag til bog/antologi/rapport/konference-proceedingKonferencebidrag i proceedingsForskningpeer 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. I Fermüller CG, Voronkov A, red., International Conference on Logic for Programming Artificial Intelligence and Reasoning. Springer. 2010. s. 217-232. (Lecture Notes in Computer Science, Bind 6397). https://doi.org/10.1007/978-3-642-16242-8_16