This paper proposes the use of abstraction by language projection to improve the performance of compositional verification to prove or disprove that a large system of composed finite-state machines satisfies a given safety property. Algorithms are presented for the automatic verification of language inclusion and controllability for discrete event systems, and are applied to a set realistic industrial examples. The experimental results suggest that the method can improve performance considerably, particularly in cases where previous methods of compositional verification fail because a large number of automata need to be considered.