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

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