ZDDs: A data structure for families of sets

From the little I've delved into BDDs, they are incredible data structures. I find Decision Diagrams in general fascinating for macro-enabled languages where they can be compiled into very efficient conditional branching code.

I gather they are used by some forms of program verification software. Beyond that, I dunno.

Although these days that industry is moving towards sat solvers.

I wouldn't consider this "industry," but they're used in some classes at CMU for program verification of student's assignments.

The canonical example is 15-213 (Intro Computer Systems). That class was also created by Dr. Randall Bryant, who (I believe) invented BDD's.

I haven't used them personally, but my understanding is that BDD's are increasingly used for formal hardware verification.