The core mechanism of abstract interpretation based program analysis consists in approximating a process of collecting more and more behaviors until reaching a fixpoint. When considering program values this process results in relations between values, and the precise approximation of such behaviors requires relations that can express disjunctions in some way. This expressiveness is necessarily limited in order to scale up and in the Astrée analyzer we developed some relations that could express disjunctions, such as the trace partitioning domain. Recent examples presented cases where those domains could not scale, because they introduced too many disjunctions. So we developed more powerful relations that express disjunctions based on segmentations.

Segmentations can be seen as ordered partitions where the boundaries can be arbitrary expressions. The use of expressions allows good expressiveness, whereas the ordering imposes constraints on the disjunction which allow efficient computation and representation. Those relations can be parameterized in order to tune the cost and the precision. They have applications for simple numerical variables but also for arrays, which where either very imprecisely handled or very costly in Astrée.

The main subject of this talk is joint work with Patrick Cousot and Radhia Cousot.