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
AN - SCOPUS:79251545789
SN - 9783642182747
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
T2 - 12th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2011
Y2 - 23 January 2011 through 25 January 2011
ER -