TP 4 - 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.

Before doing anything, please make sure to install the APRON library (using opam install apron) and to add apron and apron.polkaMPQ as libraries in the dune file of your interpreter.

In the previous session, you developed an interval analyzer. In this session, you have to:

• reuse the iterator built during the previous sessions. Ideally, there should be minimal change. The iterator should be generic enough to support both intervals and polyhedra.
• build an abstract domain for polyhedra. The domain should use internally the APRON library (you are not asked to implement polyhedral operators yourself, only to bind your analyzer to the APRON library).
• test your analyzer and evaluate experimentally on simple examples the precision improvements brought by a relational analysis.

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.

Documentation

• the APRON library documentation
• some advice on the course slides
• some more advice on the analysis project page