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
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)0302-9743
ISSN (Electronic)1611-3349

Other

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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'Decision procedures for automating termination proofs'. Together they form a unique fingerprint.

Cite this