Proving Termination of Integer Term Rewriting

DOI10.1007/978-3-642-02348-4_3MaRDI QIDQ3636817zbMATH OpenOpenAlexFDO

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

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

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

Recommendations

• Termination of term rewriting using dependency pairs
• A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs
• Termination Analysis by Dependency Pairs and Inductive Theorem Proving
• Proving termination by dependency pairs and inductive theorem proving
• Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures

Cites work

• Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages
• Automated termination proofs for logic programs by term rewriting
• Automating the dependency pair method
• Computer Aided Verification
• Constraint-Based Approach for Analysis of Hybrid Systems
• Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures
• scientific article; zbMATH DE number 1701751 (Why is no real title available?)
• scientific article; zbMATH DE number 1903370 (Why is no real title available?)
• Inference of termination conditions for numerical loops in Prolog
• Logic for Programming, Artificial Intelligence, and Reasoning
• Maximal Termination
• Mechanizing and improving dependency pairs
• Modular termination proofs for rewriting using dependency pairs
• Proving Termination by Bounded Increase
• Ranking Abstractions
• SAT Solving for Termination Analysis with Polynomial Interpretations
• Static Analysis
• Termination of logic programs: Transformational methods revisited
• Termination of term rewriting using dependency pairs
• Testing positiveness of polynomials
• Transition invariants and transition predicate abstraction for program termination
• Tyrolean termination tool: techniques and features
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation

Cited in

(14)

• Loop detection by logically constrained term rewriting
• From Jinja bytecode to term rewriting: a complexity reflecting transformation
• Runtime complexity analysis of logically constrained rewriting
• Analyzing program termination and complexity automatically with \textsf{AProVE}
• Automatically proving termination and memory safety for programs with pointer arithmetic
• Termination graphs for Java bytecode
• SAT-based termination analysis using monotonicity constraints over the integers
• Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures
• scientific article; zbMATH DE number 3921958 (Why is no real title available?)
• Completion for logically constrained rewriting
• A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs
• On proving termination of constrained term rewrite systems by eliminating edges from dependency graphs
• Verifying procedural programs via constrained rewriting induction
• From innermost to full probabilistic term rewriting: almost-sure termination, complexity, and modularity

Describes a project that uses

Uses Software

• Haskell
• Tyrolean
• AProVE

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

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