SICS Swedish Institute of Computer Science


Program Analysis by Abstract Interpretation



Analysis of a program generates a statement about the possible execution states, often expressed as annotations to the program. The statement is approximate but should be provably "safe" wrt to the operational semantics. ("safe" means that at least all possible computations are covered).

Analysis by abstract interpretation was first proposed by Patrick and Radhia Cousot [POPL'77] for use in imperative programming languages. Casting the analysis as abstract interpretation is a way of formally motivating the statement that an analysis produces "safe" approximations of the computations that can occur for a program. The method has since been used as the basis for analysis work also in both functional and logic programming languages.

A theoretic area of current importance is that of designing operators for transformation of domains, and the algebraic understanding of abstract interpretation, as for instance covered by Giacobazzi and Scozzari in "A Logical Model for Relational Abstract Domains", ACM tr. on. Prog. Lang. and Sys. sep 1998, v.20. no. 5 pp 1067--1109.

Applications of abstract interpretation include providing information to a compiler which helps it to produce better code, e.g. for compile-time garbage collection or as a tool for a programmer checking whether the program is at risk of producing unexpected data or reaching unexpected states.

An analyser based on abstract interpretation has a fixpoint solver and a set of domain functions as central components.

There are also approaches where the analysis is transformed into a constraint problem.

Links

  • A bibliography on abstract interpretation for logic programming is handled by Marc-Michel Corsini at LaBri, Bordeaux, France.
  • Dagstuhl seminar on Abstract Interpretation
  • Semantics-Based Program Analysis and Manipulation gives pointers to several analysis projects world-wide.
  • ParForce
  • ESPRIT Project
  • Manuel Hermenegildo
  • German Puebla
  • Patrick Cousot
  • German Vidal's related links
  • Andy King, A.M.King@ukc.ac.uk
  • Ulf Nilsson, ulfni@ida.liu.se
  • Joxan Jaffar
  • Annalisa Bossi
  • Sabina Rossi
  • Harald Søndergaard's papers
  • Program Analysis via Constraint Solving
  • The Program Analysis and Verification Group at Stanford works on modelling true concurrency with another approach.
  • Papers about Stan
  • Analysis and Optimization of Logic Programs, course by Saumya Debray
  • Constraint Systems for Pattern Analysis of Constraint Logic-Based Languages, Roberto Bagnara
  • Thomas Jensen's papers
  • JSP

  • Analysis of types and aliases

    At SICS we have designed and implemented different experimental analysis programs for types and aliases in logic programs and AKL programs. All of these, and some variants that are not yet implemented, are described, and soundness of the major ones is proven, in my forthcoming thesis. (The variants are all motivated by a wish to achieve more precise analysis covering polymorphism, abstract entailment as well as other domains than types and aliases. There is also a simpler analysis scheme for sequential logic programs).

    Recent Reports and Presentations

  • Sound and efficient analysis of the CCP Language AKL. Thomas Sjöland. In Dagstuhl Seminar on Concurrent Constraint Programming - The Next Ten Years. Schloss Dagstuhl, Germany, Oct 1997. Vijay Saraswat et.al. (org.). Slides.
  • Sound and efficient analysis of the CCP Language AKL - the quick story. Thomas Sjöland. In Seminar on Programming Language Implementation. Teleinformatik, KTH, Stockholm, 30 Sep 1997. Björn Lisper (org.). Slides.
  • A Domain Independent Framework for the Analysis of AKL. Per Brand and Thomas Sjöland. Extended Abstract in Fifth Compulog Network Area Meeting on Language Design and Analysis Methods. , Giorgio Levi and Maurizio Gabrielli (eds.). Università di Pisa, 1996. Slides.
  • Efficient Analysis of Type and Alias Information for a Concurrent Constraint Language. (Per Brand, Dan Sahlin, Erik Schön and Thomas Sjöland). Presentation in Analysis and Verification of Multiple-Agent Languages. Fifth LOMAPS Workshop. Abstracts. , Mads Dam and Fredrik Orava (eds.). SICS Research Report R96:05. Slides from the presentation.
  • ParForce deliverable D.WP2.3.5.M3: Assessment of a Storage Optimization Tool for AKL. Per Brand, Dan Sahlin and Thomas Sjöland. Slides on the assessment of our analysis system.
  • ParForce deliverable D.WP2.1.3.M3:On the Computation of Fixpoint in Static Program Analysis with an Application to Analysis of AKL. Erik Schön. (Master's thesis, KTH).
  • Fixpoint Analysis of Types and Alias in AKL Programs (w. D. Sahlin), (abstract).
    SICS report R94/13b. (final update 950628 of deliverable D.WP1.6.1.M2 in ParForce).

    Accesses since May 24, 1996:

    Thomas Sjöland