SPLIT is a compositional LTL verifier that is used for verifying shared-variable, multi-threaded programs. It implements the techniques of
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.
- Jan 23, 2010: version 1.0.1 is now available. This version includes a better method for verifying general LTL properties.