The authors present a compositional method for the verification of component-based systems described in a subset of the behaviour-interaction- priority language encompassing multi-party interaction without data transfer. The method is based on the use of two kinds of invariants. Component invariants are over-approximations of components' reachability sets. Interaction invariants are global constraints on the states of components involved in interactions. The method has been implemented in the D-Finder tool and has been applied for checking deadlock-freedom. The experimental results on non-trivial examples show that this method allows either to prove deadlock-freedom or to identify very few deadlock configurations that can be analysed by using state-space exploration. © 2010 The Institution of Engineering and Technology.