Proving Reachability Properties on Term Rewriting Systems with Strategies

Thomas Genet (1) , Yann Salmon (1)

1 CELTIQUE - Software certification with semantic analysis

We aim at defining regular over-approximation of sets of reachable terms for term rewriting systems applied with a strategy. In this ongoing work, we focus on innermost strategies which are the evaluation strategy of most functional programming languages. Having an accurate over-approximation of reachable terms for functional programming lan-guages would permit to prove richer unreachability properties, i.e. safety properties on such programs.

Mots clés: Term Rewriting; Tree Automata; Strategy; Tree Automata Completion

Domaines: Génie logiciel [cs.SE]; Langage de programmation [cs.PL]; Logique en informatique [cs.LO]; Théorie et langage formel [cs.FL]

Thomas Genet, Yann Salmon. Proving Reachability Properties on Term Rewriting Systems with Strategies. Workshop on Strategies in Rewriting, Proving and Programming, 2012, London, United Kingdom. ⟨hal-01111038⟩