Constant runtime complexity of term rewriting is semi-decidable

DOI10.1016/j.ipl.2018.06.012zbMath1478.68111OpenAlexW2884561268WikidataQ129515122 ScholiaQ129515122MaRDI QIDQ1799562

Jürgen Giesl, Florian Frohn

Publication date: 19 October 2018

Published in: Information Processing Letters (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ipl.2018.06.012

zbMATH Keywords

computational complexitydecidabilityformal methodsterm rewritingprogram correctness

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Grammars and rewriting systems (68Q42) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Uses Software

• AProVE
• TcT

Cites Work

• Unnamed Item
• Termination of narrowing revisited
• The finite power property for context-free languages
• From Jinja bytecode to term rewriting: a complexity reflecting transformation
• Analyzing innermost runtime complexity of term rewriting by dependency pairs
• Analyzing program termination and complexity automatically with \textsf{AProVE}
• Lower bounds for runtime complexity of term rewriting
• On Forward Closure and the Finite Variant Property
• Termination Competition (termCOMP 2015)
• Automated Complexity Analysis Based on the Dependency Pair Method
• Term Rewriting and All That
• Complexity Analysis for Java with AProVE
• Termination proofs and the length of derivations
• Modular Complexity Analysis for Term Rewriting

This page was built for publication: Constant runtime complexity of term rewriting is semi-decidable