Semantics and application to program verification

TP3 - Interval analysis

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

In addition to the provided front-end, the analyzer consists in two modules:

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


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.).

Interval domain

We suggest that you create two modules:

Additional advice is available at the end of this week's course and in the project page.

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.

Author: Antoine Miné