ENS — Semantics and applications to verification

TP4 - Relational analysis

Comes mainly from here.Thanks Antoine!

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. However, the Apron library is not documented and terrible to use. So you will write from scratch your own equality abstract domain.

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

  • Build an abstract domain for equality. Since it is a relational domain, it is an implemntation of Environment.
  • 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





Protip

Ajoutez

                            
                                eval $(opam config env)
                            
                        

à votre .bashrc (ou .zshrc, ...) pour ne plus avoir de problème avec OCaml.