Proving Termination of Integer Term Rewriting

DOI10.1007/978-3-642-02348-4_3zbMath1242.68131OpenAlexW1505286461MaRDI QIDQ3636817

Peter Schneider-Kamp, Carsten Fuhs, Stephan Falke, Martin Plücker, Jürgen Giesl

Publication date: 30 June 2009

Published in: Rewriting Techniques and Applications (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-02348-4_3

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Grammars and rewriting systems (68Q42)

Related Items (11)

Verifying Procedural Programs via Constrained Rewriting Induction ⋮ Analyzing program termination and complexity automatically with \textsf{AProVE} ⋮ Automatically proving termination and memory safety for programs with pointer arithmetic ⋮ Loop detection by logically constrained term rewriting ⋮ From Jinja bytecode to term rewriting: a complexity reflecting transformation ⋮ Unnamed Item ⋮ A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs ⋮ Termination Graphs for Java Bytecode ⋮ On Proving Termination of Constrained Term Rewrite Systems by Eliminating Edges from Dependency Graphs ⋮ SAT-based termination analysis using monotonicity constraints over the integers ⋮ Runtime complexity analysis of logically constrained rewriting

Uses Software

• Haskell
• Tyrolean
• AProVE

Cites Work

• Unnamed Item
• Unnamed Item
• Tyrolean termination tool: techniques and features
• Mechanizing and improving dependency pairs
• Testing positiveness of polynomials
• Modular termination proofs for rewriting using dependency pairs
• Termination of term rewriting using dependency pairs
• Automating the dependency pair method
• Automated termination proofs for logic programs by term rewriting
• Transition Invariants and Transition Predicate Abstraction for Program Termination
• Constraint-Based Approach for Analysis of Hybrid Systems
• Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures
• Maximal Termination
• Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages
• Proving Termination by Bounded Increase
• SAT Solving for Termination Analysis with Polynomial Interpretations
• Inference of termination conditions for numerical loops in Prolog
• Ranking Abstractions
• Logic for Programming, Artificial Intelligence, and Reasoning
• Verification, Model Checking, and Abstract Interpretation
• Computer Aided Verification
• Static Analysis
• Verification, Model Checking, and Abstract Interpretation
• Termination of logic programs: Transformational methods revisited

This page was built for publication: Proving Termination of Integer Term Rewriting