Institutional Login
Welcome!
To use the personalized features of this site, please
log in
or
register
.
If you have forgotten your username or password, we can
help
.
My Menu
Marked Items
Alerts
Order History
Saved Items
All
Favorites
Content Types
All
Publications
Journals
Book Series
Books
Reference Works
Protocols
Subject Collections
Architecture and Design
Behavioral Science
Biomedical and Life Sciences
Business and Economics
Chemistry and Materials Science
Computer Science
Earth and Environmental Science
Engineering
Humanities, Social Sciences and Law
Mathematics and Statistics
Medicine
Physics and Astronomy
Professional and Applied Computing
中文(简体)
中文(繁體)
English
Deutsch
한국어
日本語
Français
Español
العربية
Русский
Book Chapter
A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs
Book Series
Lecture Notes in Computer Science
Publisher
Springer Berlin / Heidelberg
ISSN
0302-9743 (Print) 1611-3349 (Online)
Volume
Volume 5663/2009
Book
Automated Deduction – CADE-22
DOI
10.1007/978-3-642-02959-2
Copyright
2009
ISBN
978-3-642-02958-5
DOI
10.1007/978-3-642-02959-2_22
Pages
277-293
Subject Collection
Computer Science
SpringerLink Date
Sunday, July 26, 2009
Add to marked items
Add to shopping cart
Add to saved items
Permissions & Reprints
Recommend this chapter
PDF (286.7 KB)
Free Preview
A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs
Stephan Falke
20
and Deepak Kapur
20
(20)
CS Department, University of New Mexico, Albuquerque, NM, USA
Abstract
An approach based on term rewriting techniques for the automated termination analysis of imperative programs operating on integers is presented. An imperative program is transformed into rewrite rules with constraints from quantifier-free Presburger arithmetic. Any computation in the imperative program corresponds to a rewrite sequence, and termination of the rewrite system thus implies termination of the imperative program. Termination of the rewrite system is analyzed using a decision procedure for Presburger arithmetic that identifies possible chains of rewrite rules, and automatically generated polynomial interpretations are used to show finiteness of such chains. An implementation of the approach has been evaluated on a large collection of imperative programs, thus demonstrating its effectiveness and practicality.
Partially supported by NSF grants CCF-0541315 and CNS-0831462.
Stephan
Falke
Email:
spf@cs.unm.edu
Deepak
Kapur
Email:
kapur@cs.unm.edu
Fulltext Preview (Small,
Large
)
References secured to subscribers.
more options
Find
Query Builder
Close
|
Clear
Title (ti)
Summary (su)
Author (au)
ISSN (issn)
ISBN (isbn)
DOI (doi)
And
Or
Not
(
)
* (wildcard)
"" (exact)
Within all content
Within this book series
Within this book
Export this chapter
Export this chapter as
RIS
|
Text
Frequently asked questions
|
General information on journals and books
|
Send us your feedback
|
Impressum
|
Contact
© Springer.
Part of Springer Science+Business Media
Privacy, Disclaimer, Terms and Conditions, © Copyright Information
MetaPress Privacy Policy
Remote Address: 38.107.191.81 • Server: mpweb05
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)