Roberto, Margherita and Beatrice

Home

Personal Info

Papers

Teaching

Links

On the Design of Generic Static Analyzers for Imperative Languages (TR)

Roberto Bagnara
Dipartimento di Matematica e Informatica
Università di Parma
Parco Area delle Scienze 53/A
I-43124 Parma
Italy

Patricia M. Hill
School of Computing
University of Leeds
Leeds, LS2 9JT
United Kingdom

Andrea Pescetti
Dipartimento di Matematica
Università di Parma
Parco Area delle Scienze 53/A
I-43124 Parma
Italy

Enea Zaffanella
Dipartimento di Matematica e Informatica
Università di Parma
Parco Area delle Scienze 53/A
I-43124 Parma
Italy

Abstract

The design and implementation of precise static analyzers for significant fragments of imperative languages like C, C++, Java and Python is a challenging problem. In this paper, we consider a core imperative language that has several features found in mainstream languages such as those including recursive functions, run-time system and user-defined exceptions, and a realistic data and memory model. For this language we provide a concrete semantics ---characterizing both finite and infinite computations--- and a generic abstract semantics that we prove sound with respect to the concrete one. We say the abstract semantics is generic since it is designed to be completely parametric on the analysis domains: in particular, it provides support for relational domains (i.e., abstract domains that can capture the relationships between different data objects). We also sketch how the proposed methodology can be extended to accommodate a larger language that includes pointers, compound data objects and non-structured control flow mechanisms. The approach, which is based on structured, big-step G^\infty SOS operational semantics and on abstract interpretation, is modular in that the overall static analyzer is naturally partitioned into components with clearly identified responsibilities and interfaces, something that greatly simplifies both the proof of correctness and the implementation.


Available: PDF, 300 DPI, 600 DPI, and 1200 DPI PostScript, DVI, BibTeX entry.

[Page last updated on June 06, 2008, 16:49:31.]

© Roberto Bagnara
bagnara@cs.unipr.it

Home | Personal | Papers | Teaching | Links