Termination criteria for tree automata completion

DOI10.1016/j.jlamp.2015.05.003zbMath1356.68132OpenAlexW2256367468MaRDI QIDQ730470

Thomas Genet

Publication date: 28 December 2016

Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlamp.2015.05.003

zbMATH Keywords

regular tree languagestree automataterm rewritinganalysis of functional programsregularity preservationtree automata completion

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Functional programming and lambda calculus (68N18) Grammars and rewriting systems (68Q42)

Related Items (5)

Unnamed Item ⋮ Descendants of a recognizable tree language for prefix constrained linear monadic term rewriting with position cutting strategy ⋮ Unnamed Item ⋮ Some decidability results on one-pass reductions ⋮ Pattern eliminating transformations

Uses Software

• AVISPA
• Maude
• Timbuk
• OCaml

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Reachability analysis over term rewriting systems
• Flow analysis of lazy higher-order functional programs
• Equational abstractions
• A theoretical limit for safety verification techniques with regular fix-point computations
• Equational approximations for tree automata completion
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Deterministic tree pushdown automata and monadic tree rewriting systems
• Linear generalized semi-monadic rewrite systems effectively preserve recognizability
• Tree automata for rewrite strategies
• Towards Static Analysis of Functional Programs Using Tree Automata Completion
• Characterizing Conclusive Approximations by Logical Formulae
• Certifying a Tree Automata Completion Checker
• HANDLING NON LEFT-LINEAR RULES WHEN COMPLETING TREE AUTOMATA
• Bottom-up tree pushdown automata and rewrite systems
• Decidable approximations of term rewriting systems
• Finite Models vs Tree Automata in Safety Verification
• Closure of Tree Automata Languages under Innermost Rewriting
• Decidable call by need computations in term rewriting (extended abstract)
• Higher-order multi-parameter tree transducers and recursion schemes for program verification
• A Completion Algorithm for Lattice Tree Automata
• Improved Functional Flow and Reachability Analyses Using Indexed Linear Tree Grammars
• Left-linear Bounded TRSs are Inverse Recognizability Preserving
• Model Checking Higher-Order Programs
• Verifying higher-order functional programs with pattern-matching algebraic data types
• Rewriting Approximations for Fast Prototyping of Static Analyzers
• Tree generating regular systems
• Term Rewriting and Applications
• Computer Aided Verification
• Rewriting Techniques and Applications

This page was built for publication: Termination criteria for tree automata completion