Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Conferences, Workshops, Symposiums, and Seminars
  4. Decision Procedures for Automating Termination Proofs
 
conference paper

Decision Procedures for Automating Termination Proofs

Piskac, Ruzica  
•
Wies, Thomas
2011
Verification, Model Checking, And Abstract Interpretation
12th International Conference on Verification, Model Checking, and Abstract Interpretation

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.

  • Details
  • Metrics
Type
conference paper
DOI
10.1007/978-3-642-18275-4_26
Web of Science ID

WOS:000297039800026

Author(s)
Piskac, Ruzica  
Wies, Thomas
Date Issued

2011

Publisher

Springer-Verlag New York, Ms Ingrid Cunningham, 175 Fifth Ave, New York, Ny 10010 Usa

Published in
Verification, Model Checking, And Abstract Interpretation
ISBN of the book

978-3-642-18274-7

Series title/Series vol.

Lecture Notes in Computer Science; 6538

Start page

371

End page

386

Subjects

Decidability

•

Abstraction

Editorial or Peer reviewed

NON-REVIEWED

Written at

EPFL

EPFL units
LARA  
Event nameEvent placeEvent date
12th International Conference on Verification, Model Checking, and Abstract Interpretation

Austin, TX

Jan 23-25, 2011

Available on Infoscience
December 16, 2011
Use this identifier to reference this record
https://infoscience.epfl.ch/handle/20.500.14299/73272
Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés