Reachability, confluence, and termination analysis with state-compatible automata

DOI10.1016/j.ic.2016.06.011zbMath1362.68137OpenAlexW2410859016MaRDI QIDQ515687

Bertram Felgenhauer, René Thiemann

Publication date: 16 March 2017

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2016.06.011

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Grammars and rewriting systems (68Q42)

Related Items (4)

Automatic refinement to efficient data structures: a comparison of two approaches ⋮ First-order theory of rewriting for linear variable-separated rewrite systems: automation, formalization, certification ⋮ Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting ⋮ Unnamed Item

Uses Software

• Isabelle
• Isabelle/HOL
• Timbuk
• CeTA
• Tyrolean
• CSI
• Archive Formal Proofs
• Tree Automata
• Light-weight Containers

Cites Work

• Reachability analysis over term rewriting systems
• On tree automata that certify termination of left-linear term rewriting systems
• Match-bounds revisited
• Isabelle/HOL. A proof assistant for higher-order logic
• Certification of Termination Proofs Using CeTA
• Certifying a Tree Automata Completion Checker
• Code Generation via Higher-Order Rewrite Systems
• Local Termination
• CSI – A Confluence Tool
• Light-Weight Containers for Isabelle: Efficient, Extensible, Nestable
• Reachability Analysis with State-Compatible Automata
• Term Rewriting and Applications
• The Isabelle Collections Framework

This page was built for publication: Reachability, confluence, and termination analysis with state-compatible automata