Decision procedures for automating termination proofs

Ruzica Piskac, Thomas Wies

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Automated termination provers often use the following schema to prove that a program terminates: construct a relational abstraction of the program's transition relation and then show that the relational abstraction is well-founded. The focus of current tools has been on developing sophisticated techniques for constructing the abstractions while relying on known decidable logics (such as linear arithmetic) to express them. We believe we can significantly increase the class of programs that are amenable to automated termination proofs by identifying more expressive decidable logics for reasoning about well-founded relations. We therefore present a new decision procedure for reasoning about multiset orderings, which are among the most powerful orderings used to prove termination. We show that, using our decision procedure, one can automatically prove termination of natural abstractions of programs.

Original languageEnglish (US)
Title of host publicationVerification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Proceedings
Pages371-386
Number of pages16
Volume6538 LNCS
DOIs
StatePublished - 2011
Event12th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2011 - Austin, TX, United States
Duration: Jan 23 2011Jan 25 2011

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6538 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other12th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2011
CountryUnited States
CityAustin, TX
Period1/23/111/25/11

Fingerprint

Decision Procedures
Termination
Reasoning
Logic
Multiset
Terminate
Schema
Express
Abstraction

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Piskac, R., & Wies, T. (2011). Decision procedures for automating termination proofs. In Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Proceedings (Vol. 6538 LNCS, pp. 371-386). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6538 LNCS). https://doi.org/10.1007/978-3-642-18275-4_26

Decision procedures for automating termination proofs. / Piskac, Ruzica; Wies, Thomas.

Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Proceedings. Vol. 6538 LNCS 2011. p. 371-386 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6538 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Piskac, R & Wies, T 2011, Decision procedures for automating termination proofs. in Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Proceedings. vol. 6538 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 6538 LNCS, pp. 371-386, 12th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2011, Austin, TX, United States, 1/23/11. https://doi.org/10.1007/978-3-642-18275-4_26
Piskac R, Wies T. Decision procedures for automating termination proofs. In Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Proceedings. Vol. 6538 LNCS. 2011. p. 371-386. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-18275-4_26
Piskac, Ruzica ; Wies, Thomas. / Decision procedures for automating termination proofs. Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Proceedings. Vol. 6538 LNCS 2011. pp. 371-386 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{a37fa88473754f40b9aecf47b6186e0f,
title = "Decision procedures for automating termination proofs",
abstract = "Automated termination provers often use the following schema to prove that a program terminates: construct a relational abstraction of the program's transition relation and then show that the relational abstraction is well-founded. The focus of current tools has been on developing sophisticated techniques for constructing the abstractions while relying on known decidable logics (such as linear arithmetic) to express them. We believe we can significantly increase the class of programs that are amenable to automated termination proofs by identifying more expressive decidable logics for reasoning about well-founded relations. We therefore present a new decision procedure for reasoning about multiset orderings, which are among the most powerful orderings used to prove termination. We show that, using our decision procedure, one can automatically prove termination of natural abstractions of programs.",
author = "Ruzica Piskac and Thomas Wies",
year = "2011",
doi = "10.1007/978-3-642-18275-4_26",
language = "English (US)",
isbn = "9783642182747",
volume = "6538 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "371--386",
booktitle = "Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Proceedings",

}

TY - GEN

T1 - Decision procedures for automating termination proofs

AU - Piskac, Ruzica

AU - Wies, Thomas

PY - 2011

Y1 - 2011

N2 - Automated termination provers often use the following schema to prove that a program terminates: construct a relational abstraction of the program's transition relation and then show that the relational abstraction is well-founded. The focus of current tools has been on developing sophisticated techniques for constructing the abstractions while relying on known decidable logics (such as linear arithmetic) to express them. We believe we can significantly increase the class of programs that are amenable to automated termination proofs by identifying more expressive decidable logics for reasoning about well-founded relations. We therefore present a new decision procedure for reasoning about multiset orderings, which are among the most powerful orderings used to prove termination. We show that, using our decision procedure, one can automatically prove termination of natural abstractions of programs.

AB - Automated termination provers often use the following schema to prove that a program terminates: construct a relational abstraction of the program's transition relation and then show that the relational abstraction is well-founded. The focus of current tools has been on developing sophisticated techniques for constructing the abstractions while relying on known decidable logics (such as linear arithmetic) to express them. We believe we can significantly increase the class of programs that are amenable to automated termination proofs by identifying more expressive decidable logics for reasoning about well-founded relations. We therefore present a new decision procedure for reasoning about multiset orderings, which are among the most powerful orderings used to prove termination. We show that, using our decision procedure, one can automatically prove termination of natural abstractions of programs.

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

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

U2 - 10.1007/978-3-642-18275-4_26

DO - 10.1007/978-3-642-18275-4_26

M3 - Conference contribution

SN - 9783642182747

VL - 6538 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 371

EP - 386

BT - Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Proceedings

ER -