This paper introduces separation predicates, a technique to reuse some ideas from separation logic in the framework of program veri cation using a traditional rst-order logic. The purpose is to bene t from existing speci cation languages, veri cation condition generators, and automated theorem provers. Separation predicates are automatically derived from user-de ned inductive predicates. We illustrate this idea on a non-trivial case study, namely the composite pattern, which is speci- ed in C/ACSL and veri ed in a fully automatic way using SMT solvers Alt-Ergo, CVC3, and Z3.