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. We suggest implementing a domain able to abstract a set of integers into a parity information (VALUE_DOMAIN signature), and apply it to the generic NonRelational functor we developed in the previous sessions, able to lift a VALUE_DOMAIN into an ENVIRONMENT_DOMAIN by assigning an abstract property independently to each variable.


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

Note that there are two choices: we can either develop a reduction at the ENVIRONMENT_DOMAIN level, or at the VALUE_DOMAIN level (as seen in the course). The later is simpler but is limited to non-relational domains. Nevertheless, we suggest working at the VALUE_DOMAIN level for simplicity, as this is all what is needed to combine intervals and parities.

Ideally, the reduced product is then a generic functor ReducedProduct taking three arguments:

  • a first abstract domain module A:VALUE_DOMAIN;
  • a second abstract domain module B:VALUE_DOMAIN;
  • a module containing only the reduction function between the two domains: val reduce: A.t -> B.t -> A.t * B.t

and the functor outputs a module of signature VALUE_DOMAIN.

(equivalently, the functor can take a single module argument that packs the two abstract domains and a reduction function)

That way, given two existing domain implementations, building their reduced product boils down to implementing only one new module, with a single function.



                                eval $(opam config env)

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