Symbolic Data Structure for Sets of k-uples of Integers
Pierre Ganty, Cédric Meuter, Laurent Van Begin, Gabriel Kalyon, Jean-François Raskin, Giorgio Delzanno · 2007
Abstract. In this document we present a new symbolic data structure dedicated to the manipulation of (possibly infinite) sets of k-uples over integers, initially introduced in [Gan02]. This new data structure called Interval Sharing Tree (IST), is based on sharing trees [ZL95] where each node is labelled with an interval of integers. We present symbolic algo-rithm on IST for standard set operations and also introduce some specific operation that can be useful in the context of model-checking. 1