Decision Procedures for Automating Termination Proofs

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.


Published in:
Verification, Model Checking, And Abstract Interpretation, 6538, 371-386
Presented at:
12th International Conference on Verification, Model Checking, and Abstract Interpretation, Austin, TX, Jan 23-25, 2011
Year:
2011
Publisher:
Springer-Verlag New York, Ms Ingrid Cunningham, 175 Fifth Ave, New York, Ny 10010 Usa
ISBN:
978-3-642-18274-7
Keywords:
Laboratories:




 Record created 2011-12-16, last modified 2018-03-17


Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)