romain.demangeon (at) nulllip6.fr
An abstract domain for trees with numeric relations
Speaker(s) : Matthieu Journault (LIP6 - APR)We will present the definition of an abstract domain able to infer invariants on programs manipulating trees. Trees are defined over a finite alphabet and can contain unbounded numeric values at their leaves. The domain can infer the possible shapes of the tree values of each variable and find numeric relations between: the values at the leaves as well as the size and depth of the tree values of different variables. The abstract domain is described as a product of (1) a symbolic domain based on a tree automata representation and (2) a numerical domain lifted, for the occasion, to describe numerical maps with potentially infinite and heterogeneous definition set. We will present possible applications, such as the ability to describe memory zones, track symbolic equalities between program variables, or describe memory state of tree manipulating program.