The aim of this thesis is to describe the semantics of a process calculus by means of hypergraph rewriting, creating a specification mechanism combining modularity of process calculi and locality of graph transformation. Verification of processes is addressed by presenting two methods: barbed congruence for relating processes displaying the same behaviour and generic type systems. The generic type system is a framework which can be instantiated in order to check a property (e.g. absence of deadlocks, confluence, privacy). The type system satisfies the subject reduction property, has principal types and allows automated type inference.