SPLIT: A Compositional LTL Verifier

This paper describes SPLIT, a compositional verifier for safety and general LTL properties of shared-variable, multi-threaded programs. The foundation is a computation of compact local invariants, one for each process, which are used for constructing a proof for the property. An automatic refinement procedure gradually exposes more local information, until a decisive result (proof/disproof) is obtained.