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.


Publié dans:
Verification, Model Checking, And Abstract Interpretation, 6538, 371-386
Présenté à:
12th International Conference on Verification, Model Checking, and Abstract Interpretation, Austin, TX, Jan 23-25, 2011
Année
2011
Publisher:
Springer-Verlag New York, Ms Ingrid Cunningham, 175 Fifth Ave, New York, Ny 10010 Usa
ISBN:
978-3-642-18274-7
Mots-clefs:
Laboratoires:




 Notice créée le 2011-12-16, modifiée le 2020-07-30


Évaluer ce document:

Rate this document:
1
2
3
 
(Pas encore évalué)