Nowadays, refactoring is becoming a more and more common re-engineering practice. Many different tools already provide their own implementation of a set of popular refactorings, but general formal support for refactoring is still lacking. We present how graphs and graph transformation can be a suitable approach for a formal, language indepent specification of a refactoring, and which benefits such a specification has for proving the preservation of certain behavioural properties of a program, and for automatic tool support.