Automatic Proofs of Termination With Elementary Interpretations

DOI10.1016/j.entcs.2009.12.004zbMath1294.68058MaRDI 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 analysis; termination; constraint solving; elementary interpretations

Mathematics Subject Classification ID

68Q60: Specification and verification (program logics, model checking, etc.)

68Q42: Grammars and rewriting systems

68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Related Items

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

Uses Software

• REVE

Cites Work

• 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
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item