Slicing is a programanalysis technique, originally aimed at helping software engineers in program debugging. A slic- ing algorithm is intended to remove unnecessary state- ments, with respect to a criterion. Nowadays, slicing is be- coming more important on the specification level, for model reduction. Our contribution consists of a dependence-based solution to the problem of slicing communicating automata specifications, together with efficient algorithms to auto- matically extract slices. The resulting slicing tool -- named CARVER -- has shown to be operational in specification de- bugging and understanding. The model reduction results obtained with this tool are promising, notably in the area of formal validation and verification.