A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs
From MaRDI portal
Publication:5191108
DOI10.1007/978-3-642-02959-2_22zbMath1250.68141OpenAlexW1587451605MaRDI QIDQ5191108
Publication date: 28 July 2009
Published in: Automated Deduction – CADE-22 (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-02959-2_22
Specification and verification (program logics, model checking, etc.) (68Q60) Grammars and rewriting systems (68Q42) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
Verifying Procedural Programs via Constrained Rewriting Induction, Loop detection by logically constrained term rewriting, From Jinja bytecode to term rewriting: a complexity reflecting transformation, On Proving Termination of Constrained Term Rewrite Systems by Eliminating Edges from Dependency Graphs
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Mechanically proving termination using polynomial interpretations
- Tyrolean termination tool: techniques and features
- Testing positiveness of polynomials
- Termination of term rewriting using dependency pairs
- Transition Invariants and Transition Predicate Abstraction for Program Termination
- Recursive functions of symbolic expressions and their computation by machine, Part I
- Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures
- Proving Termination by Bounded Increase
- SAT Solving for Termination Analysis with Polynomial Interpretations
- Proving Termination of Integer Term Rewriting
- Operational Termination of Conditional Rewriting with Built-in Numbers and Semantic Data Structures
- Computer Aided Verification
- 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
