Abstract Interpretation is a framework for static program analysis. The
value in an abstract comain represents a property of the program, e.g., the
set of possible states in a program point, which can be given as constraints
on the values of the program variables in that point. In general, the sets
are overapproximated by the abstract values, and it is desirable to find
approximations that are as exact as possible without the analysis using to
For numerical variables, numerical domains are used: these range from simple
intervals, over systems of linear inequalities, and polyhedra, to sets
corresponding to general Presburger formulae. The complexity of the analysis
grows extremely fast with the complexity of the domain. It is desirable to
find the right tradeoff between precision and complexity, for programs that
appear in practice.
The purpose of the thesis project is to gather more knowledge about
numerical domains, and how advanced such domains could be used to increase
the precision of the program analyses that are being developed within the
research group for programming languages at IDE. Interesting candidates may
include intervals extended with strides, or a generalization of this to
general polyhedra intersected with the subspace of integer vectors spanned
by a given set of base vectors. The project contains the following parts:
- Study of the basic theory of abstract interpretation, and the "classical"
numerical domains (intervals, polyhedra).
- A literature stury, where a comprehensive search for existing literature
in the area is made. The result of the search should be a survey, which
is to be included in the M.Sc. thesis.
- If not already present in the literature, development of a new numerical
domain with a potential to provide a suitable tradeoff between precision
and complexity. The following should be defined:
- the elements of the domain
- operations: LUB, GLB, widening, test for equality, (possibly)
narrowing, and abstract versions of common numerical operations
(arithmetic, etc.) and relations. The correctness of the abstract
operations should be proved.
- Possibly, if found suitable, a prototype implementation should be made,
within the existing WCET tool of the research group.
- Report writing, presentation.
The thesis project will be carried out within the WCET analysis project of
the research group.