In this paper, we describe a method for proving properties of parametric automata. These properties have the form p(L,S) Þ z(S)]]>, where p is a predicate characterizing the automaton, L is a list of parametric actions accepted by the automaton, S is a parametric state, and z]]> a logic formula. In previous work, we proposed a bottom-up evaluation process for computing the set of all the consequences of p(L,S), then showing that it contains z(S)]]>. Such forward reasoning methods often do not terminate. We propose here instead a backward reasoning method which is driven by the conclusion z]]>. The method consists essentially in transforming the program defining p by unfolding all the recursive clauses that do not leaveinvariant z]]>. We have successfully applied this method to the verification of some functional properties of a parametric sliding window protocol.