Loop detection by logically constrained term rewriting

DOI10.1007/978-3-030-03592-1_18zbMath1403.68107OpenAlexW2900512542MaRDI QIDQ1629968

Naoki Nishida, Sarah Winkler

Publication date: 7 December 2018

Full work available at URL: https://doi.org/10.1007/978-3-030-03592-1_18

zbMATH Keywords

loopsnonterminationconstrained rewriting

Mathematics Subject Classification ID

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

Related Items (2)

Reducing non-occurrence of specified runtime errors to all-path reachability problems of constrained rewriting ⋮ Runtime complexity analysis of logically constrained rewriting

Cites Work

• Loop detection in term rewriting using the eliminating unfoldings
• Analyzing program termination and complexity automatically with \textsf{AProVE}
• Term Rewriting with Logical Constraints
• Proving non-termination
• Proving Termination Through Conditional Termination
• Constrained Term Rewriting tooL
• Proving Termination of Integer Term Rewriting
• Term Rewriting and All That
• A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs
• Verifying Procedural Programs via Constrained Rewriting Induction
• Termination Analysis of C Programs Using Compiler Intermediate Languages

This page was built for publication: Loop detection by logically constrained term rewriting