To reason effectively about programs it is important to have some version of a transitive closure operator so that we can describe such notions as the set of nodes reachable from a program's variables. On the other hand, with a few notable exceptions, adding transitive closure to even very tame logics makes them undecidable.

In this talk I will describe the boundary between decidability and undecidability for transitive closure logics. I will also discuss the complexity of relevant decision procedures and their application to static analysis.

Much of the work I will describe comes from papers at CSL'04 and CAV'04 with Alex Rabinovich, Tom Reps, Mooly Sagiv, and Greta Yorsh.