Rewriting for Fast Prototyping of Static Analyzers

Yohan Boichut 1 Thomas Genet 1 Thomas Jensen 1 Luka Leroux 1
1 Lande - Logiciel : ANalyse et DEveloppement
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Abstract : This paper defines a new framework for fast prototyping of static analyzers based on rewriting techniques. Starting from a term rewriting system representing the operational semantics of the target programming language and given a program to analyze, we automatically construct an over-approximation of the set of reachable terms, i.e. of program states that can be reached. With this approximation, it is possible to prove a variety of safety or security properties expressible in terms of (un)reachability. Compared with static analysis based on abstract interpretation, a salient feature of this approach is that the approximation is correct by construction. The approach enables fast prototyping of static analyzers because modifying the analysis simply amounts to changing the set of rewrite rules defining the approximation. To illustrate the framework proposed here on a realistic programming language we instantiate it with the Java Virtual Machine semantics and use Java bytecode programs as running examples. We show how to compile a Java bytecode program into an equivalent term rewriting system and show how to specify and implement simple class analysis by defining rewriting approximations.
Type de document :
[Research Report] RR-5997, INRIA. 2006, pp.20
Liste complète des métadonnées
Contributeur : Rapport de Recherche Inria <>
Soumis le : lundi 16 octobre 2006 - 10:56:57
Dernière modification le : vendredi 16 novembre 2018 - 01:23:54
Document(s) archivé(s) le : lundi 20 septembre 2010 - 17:10:00



  • HAL Id : inria-00106330, version 2


Yohan Boichut, Thomas Genet, Thomas Jensen, Luka Leroux. Rewriting for Fast Prototyping of Static Analyzers. [Research Report] RR-5997, INRIA. 2006, pp.20. 〈inria-00106330v2〉



Consultations de la notice


Téléchargements de fichiers