@TechReport{BagnaraHPZ08TR,
  Author = "R. Bagnara and P. M. Hill and A. Pescetti and E. Zaffanella",
  Title = "On the Design of Generic Static Analyzers
           for Imperative Languages",
  Type = "Quaderno",
  Number = 485,
  Institution = "Dipartimento di Matematica, Universit\`a di Parma, Italy",
  Year = 2008,
  Note = "Available at \url{http://www.cs.unipr.it/Publications/}",
  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 \emph{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 $\mathrm{G}^\infty\mathrm{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."
}