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.
In the previous session, we developed an interval analyzer. In this session we will:
- 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.