Constrained Horn Clauses (CHCs) provide a suitable logical formalism for addressing a wide range of program verification problems. For this reason, a lot of effort has been recently devoted to the development of sophisticated solvers for checking the satisfiability of CHCs on various constraint theories (e.g., Linear Integer or Real Arithmetic, arrays, bitvectors, inductively defined data types). However, the effectiveness of solvers often depends on how the verification problem is encoded into clausal form, and suitable pre-processing techniques can significantly simplify the search for a satisfiability proof. In this talk we present recent and ongoing research on transformation techniques for CHCs that can be used to ease satisfiability proofs, and hence program verification. We follow a very general approach based on transformation rules such as unfolding, folding, and constraint rewriting. These rules are combined together in more complex transformation strategies, such as CHC specialization and predicate tupling. We demonstrate the usefulness of these transformations for various program verification tasks, such as proving partial correctness with respect to pre/post-conditions and proving relational properties (e.g., equivalence and non-interference). We also show that the approach based on CHC transformation is, to a large extent, language agnostic, by considering verification problems for programs written in various programming languages.