Skip to Main content Skip to Navigation

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.
Document type :
Complete list of metadata
Contributor : Rapport De Recherche Inria Connect in order to contact the contributor
Submitted on : Monday, October 16, 2006 - 10:56:57 AM
Last modification on : Friday, February 4, 2022 - 3:14:20 AM
Long-term archiving on: : Monday, September 20, 2010 - 5:10:00 PM


  • 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⟩



Record views


Files downloads