SPLIT is a compositional LTL verifier that is used for verifying shared-variable, multi-threaded programs. It implements the techniques of [1] [2] [3], [4] for verifying safety and general LTL properties. The foundation is a computation of compact local invariants, one for each process, that are used for constructing a proof for the property. If the invariants are too weak, an automatic refinement gradually exposes more local information, until the property can be proved or a valid counter example is formed.