Reachability Analysis of Innermost Rewriting

Thomas Genet 1, * Yann Salmon 1
* Auteur correspondant
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : We consider the problem of inferring a grammar describing the output of a functional program given a grammar describing its input. Solutions to this problem are helpful for detecting bugs or proving safety properties of functional programs and, several rewriting tools exist for solving this problem. However, known grammar inference techniques are not able to take evaluation strategies of the program into account. This yields very imprecise results when the evaluation strategy matters. In this work, we adapt the Tree Automata Completion algorithm to approximate accurately the set of terms reachable by rewriting under the innermost 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 show that it noticeably improves the accuracy of static analysis for functional programs using the call-by-value evaluation strategy.
Liste complète des métadonnées

Littérature citée [27 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01194530
Contributeur : Thomas Genet <>
Soumis le : lundi 7 septembre 2015 - 10:55:42
Dernière modification le : mardi 16 janvier 2018 - 15:54:17
Document(s) archivé(s) le : mardi 8 décembre 2015 - 10:49:49

Fichier

GenetSalmon-RTA15.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Thomas Genet, Yann Salmon. Reachability Analysis of Innermost Rewriting. RTA, 2015, Warshaw, Poland. pp.1-17, 2015, 〈10.4230/LIPIcs.RTA.2015.x〉. 〈hal-01194530〉

Partager

Métriques

Consultations de la notice

412

Téléchargements de fichiers

106