Automatic Proofs of Termination With Elementary Interpretations

DOI10.1016/j.entcs.2009.12.004zbMath1294.68058OpenAlexW2010033825MaRDI QIDQ5170190

Salvador Lucas

Publication date: 22 July 2014

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.12.004

zbMATH Keywords

program analysisterminationconstraint solvingelementary interpretations

Mathematics Subject Classification ID

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 (1)

Beyond polynomials and Peano arithmetic -- automation of elementary and ordinal interpretations

Uses Software

• REVE

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Termination of rewriting systems by polynomial interpretations and its implementation
• Proving termination of context-sensitive rewriting by transformation
• Context-sensitive dependency pairs
• Termination of rewriting
• Testing positiveness of polynomials
• Termination of rewrite systems by elementary interpretations
• Termination of term rewriting using dependency pairs
• Algebraic and logic programming. Third international conference, ALP '92, Volterra, Italy, September 2--4, 1992. Proceedings
• Orderings and Constraints: Theory and Practice of Proving Termination
• Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic
• Polynomials over the reals in proofs of termination : from theory to practice
• Context-Sensitive Dependency Pairs

This page was built for publication: Automatic Proofs of Termination With Elementary Interpretations