Skip to Main content Skip to Navigation
Reports

Reachability Analysis of Innermost Rewriting

Thomas Genet 1 Yann Salmon 1
1 CELTIQUE - Software certification with semantic analysis
IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL, Inria Rennes – Bretagne Atlantique
Abstract : Approximating the set of terms reachable by rewriting finds more and more applications ranging from termination proofs of term rewriting systems, cryp- tographic protocol verification to static analysis of programs. However, since approximation techniques do not take rewriting strategies into account, they build very coarse approximations when rewriting is constrained by a specific strategy. In this work, we propose to adapt the Tree Automata Completion algorithm to accurately approximate the set of terms reachable by rewriting under the inner- most strategy. We prove that the proposed technique is sound and precise w.r.t. innermost rewriting. The proposed algorithm has been implemented in the Timbuk reachability tool. Experiments shows that it noticeably improves the accuracy of static analysis for functional programs using the call-by-value evaluation strategy. In particular, for some functional programs needing lazy evaluation to terminate, the computed approximations are precise enough to prove the absence of innermost normal forms, i.e. prove non termination of the program with call-by-value.
Complete list of metadatas

Cited literature [22 references]  Display  Hide  Download

https://hal.inria.fr/hal-00848260
Contributor : Yann Salmon <>
Submitted on : Monday, February 10, 2014 - 11:28:38 PM
Last modification on : Wednesday, December 18, 2019 - 5:20:44 PM
Document(s) archivé(s) le : Sunday, April 9, 2017 - 10:42:18 AM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00848260, version 5

Citation

Thomas Genet, Yann Salmon. Reachability Analysis of Innermost Rewriting. [Research Report] 2013. ⟨hal-00848260v5⟩

Share

Metrics

Record views

1482

Files downloads

193