TP3 - Interval Analysis

Comes mainly from here and here. Thanks Antoine and Marc !

The goal of this session is to transform the denotational interpreter for our simple language into an abstract interpreter over the interval domain.

You will have to implement the iterator with widening, the environment domain for abstract values, the interval abstract domain and a very simple abstract boolean domain. But you will reuse the Value module (as well as error).

These two parts should be made into modules as independent as possible so that:

  • you can replace the interval domain with another one without changing the iterator (we will do this next week);
  • you can reuse the interval domain for the static analysis project, which uses a different input language and a different intermediate representation for programs.


The iterator should work by induction on the syntax tree of the program. It is actually very similar to the iterator we used in the denotational concrete semantics.

The main difference with the concrete semantics is the use of a widening to ensure the termination of the analysis. For this practical exercise, we will focus first on the simplest iteration techniques and then, if time allows, consider more advanced ones (widening with thresholds, decreasing iterations, etc.).

Abstract domains

We suggest that you implement the two needed modules in the following order:

  • a module abstracting sets of integers as intervals; this is module MakeInterval in
  • a module abstracting sets of boolean values; this is module Make in file domains/

You also have to implement union and widen functions and missing cases in MakeValueBasics.

Additional advice is available at the end of this week’s course.

During this practical exercise, you will only need to handle precisely simple tests, such as comparing a variable with another variable or a constant. In case the test is not simple, the analyzer should still be sound (e.g., by returning its environment argument unchanged). We leave the precise handling of arbitrary conditions for the project.