This project describes the design of a distributed implementation of the CDD data structure. CDD''s are related to BDD''s but handles interval instead binary values. The CDD is used in the real time verification tool Uppaal to store the symbolic part of its states, these states consists of both a discrete part and a symbolic part. This distribution is conducted for the primary reason of allowing verification of larger models. Besides designing the distribution of the data structure, four operations working on the data structure are designed. The semantics for the distributed data structure is described, and some semantic proofs of important properties for the operations are given.
The thesis tried to investigate, is whether using a single CDD data structure, compared to a number of smaller CDDs in a distributed verification environment, can save some memory by taking advantage of global sharing. That is, sharing in the symbolic representation, across several discrete states. Runtime is not considered as memory is the primary bottleneck in verification, the state space takes up several GB in minutes.
Finally tests are conducted to test the thesis, and to encounter the runtime penalty for these memory savings. The result shows that the memory saving were up to 70%, using a single CDD distributed over 4 nodes, compared to letting the 4 nodes holds four separate CDD''s, this memory saving comes at a runtime penalty of 560-900%.
Besides trying to save memory by distributing the CDD data structure, some design were made to represent the CDD nodes as compact as possible. The memory representation saved up to 20% of memory compared to the memory representation used in an existing implementation of the CDD data structure. The runtime penalty for this memory saving is 50%.

During the tests we discovered that the problem of memory usage in Uppaal were not the storage of the symbolic part, but storing the discrete part. In most timed automata models, the discrete part takes up the majority of the used memory. As we had focused on the distribution of the symbolic part, we were not able to verify larger models in the distributed implementation, than on a single Computer node.

In the last chapter some possible optimizations to the design/implementation is discussed. This description also includes a discussion of which part of this project might be used for other projects, trying to distribute decision diagram data structures. A possible data structure for storing the discrete part of the states, is also described briefly.