Semantics and application to program verification

TP4 - Relational analysis

The goal of this session is to analyze the language developed in the previous sessions using relational numerical abstract domains, in particular the polyhedra domain.

In the previous session, we developed an interval analyzer. In this session we will:

As the Apron library provides a generic interface, it should be easy for your analyzer to support all the other abstract domains offered by Apron (such as octagons for instance) and perform additional experiments.


  • the Apron library documentation;
  • some advice on the course slides.

    Author: Antoine Miné