BDDs is the choice of data structure for Tau at the moment. "Working like the charmest charm" says Ohad Asor. Never seen him this satisfied with an implementation before.
Video by Model Checking.
