Formally Verified Algorithms for Computing with LDDs
----------------------------------------------------

A common aspect in analysing the behaviour of (software) systems
involves constructing and manipulating a state space that compactly
represents the behaviour of the system being analysed. A state
space, which is often some form of graph, can be represented
explicitly by storing each of its individual elements in memory.
Consequently, larger state spaces require more memory.  
An alternative to an explicit representation is a symbolic
representation, which may represent the state space in a more compact
manner. The prototypical example of such a symbolic representation
is one in which Binary Decision Diagrams (BDDs) are used to represent
the sets of vertices and edges of a graph. Such representations
allow for analysing systems of phenomenal size. BDDs are typically
useful when the sizes of the relevant sets are known upfront, which
is not always the case. A symbolic data structure that does not
have this limitation is a List Decision Diagram (LDD). In this
assignment, you are asked to formalise LDDs in a theorem prover/program
analyser (think, COQ, TLA+, Daphne, etc.) and prove the correctness
of sequential (and possibly parallel) algorithms for building and
manipulating LDDs.