Using context-sensitive rewriting for proving innermost termination of rewriting

DOI10.1016/J.ENTCS.2009.07.055MaRDI QIDQ2808236zbMATHOpenAlexFDO

Authors Beatriz Alarcón, Salvador Lucas

Publication date 20 May 2016

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2009.07.055

zbMATH Keywords

terminationdependency pairsinnermost rewritingcontext-sensitive rewriting program analysis

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Grammars and rewriting systems (68Q42)

Recommendations

• Termination of Innermost Context-Sensitive Rewriting Using Dependency Pairs
• scientific article; zbMATH DE number 1948501
• Termination of context-sensitive rewriting
• Termination of rewriting with strategy annotations
• Proving termination of context-sensitive rewriting with MU-TERM

Cites work

• scientific article; zbMATH DE number 1332639 (Why is no real title available?)
• scientific article; zbMATH DE number 1948501 (Why is no real title available?)
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Automating the dependency pair method
• Context-Sensitive Dependency Pairs
• Context-sensitive rewriting strategies
• Improving the context-sensitive dependency graph
• Mechanizing and improving dependency pairs
• Proving operational termination of membership equational programs
• Proving termination of context-sensitive rewriting by transformation
• Proving termination of context-sensitive rewriting with MU-TERM
• Relaxing monotonicity for innermost termination
• Term Rewriting and Applications
• Termination of Innermost Context-Sensitive Rewriting Using Dependency Pairs
• Termination of rewriting with strategy annotations
• Termination of term rewriting using dependency pairs
• Transformation techniques for context-sensitive rewrite systems

Cited in

(8)

• Termination of Context-Sensitive Rewriting with Built-In Numbers and Collection Data Structures
• Termination of rewriting with strategy annotations
• Proving termination of context-sensitive rewriting by transformation
• A context-based approach to proving termination of evaluation
• Termination of Innermost Context-Sensitive Rewriting Using Dependency Pairs
• scientific article; zbMATH DE number 1948501 (Why is no real title available?)
• Proving termination properties with \textsc{mu-term}
• Applications and extensions of context-sensitive rewriting

Describes a project that uses

Uses Software

• OBJ3
• Maude
• MU-TERM

This page was built for publication: Using context-sensitive rewriting for proving innermost termination of rewriting

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2808236)