ENS — Semantics and applications to verification

TP5 - Reduced products

The goal of this session is to implement in our analyzer the reduced products between two simple non-relational domains: the interval domain and the parity domain.

Parity domain

A first (straightforward) step is to implement a parity domain, able to discover whether each variable is even or odd. This is an INT_DOMAIN.

Reduction

We wish to implement the reduced product in a generic way, with as few dependencies as possible on the domains we wish to combine.

To do that, we define a common constrain type, be able to produce and use them. The product of domain have to perform the reduction whenever you feel suited.





Protip

Ajoutez

                            
                                eval $(opam config env)
                            
                        

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