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).
- A precondition analyser for AKL using generic fixpoint solvers is part of the downloadable
Agents/AKL release.
The analyser generates a fixpoint problem over a domain expressing possible aliases and types at program points.
It makes use of program points at guards, bodies and literals and uses general fixpoint solvers to solve the
generated equation system. The motivation for the method goes through a step of first devising an abstracted version
of the operational semantics of AKL (a variant of the computation rules showing the possible executions of AKL in the
form given by the original designers) and relating this to the schema that generates the fixpoint problem.
Three different versions of the fixpoint solver were tested. The implementation of the analyser was originally in AKL.
Later it has also been automatically translated to Prolog giving
a more efficient system; appr. 4 times faster and
much more lean in its memory requirements (since the analyser is essentially a deterministic algorithm capable of
making use of the highly efficient SICStus Prolog compiler). The AKL analyser has been applied to all demo programs
of AKL proving its applicability on programs up to several thousand lines of AKL code.
- ParForce, ESPRIT Project in which the initial design and implementation activity (except formal proofs and refinements) was performed.
- A poster on our
analysis system.
- For comparison purposes I also implemented some algorithms for global post-condition analysis of aliases and types in logic programs
- A bottom-up algorithm based on abstracting unification of terms with set membership for abstract terms and using an obvious fixpoint algorithm to collect all possible equalities in the program.
- A rewrite algorithm collecting all equalities occurring in a normalized program and adding transition relations modeling the argument transfer occuring in calls, and then normalizing the set of equations based on this information.
- Another algorithm based on specialising clauses for possible calls as the analysis proceeds,
giving a form of polymorphism, since different variant of the program clauses generated for different calls are given different types. (based on an initial idea by Torkel Franzén).
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