The use of function specifications to reason about function calls and the manipulation of user-defined
predicates are two essential ingredients of modern compositional verification tools based on separation
logic. To execute these operations successfully, these tools must be able to solve the frame inference
problem, that is, to understand which parts of the state are relevant for the operation at hand. We
introduce matching plans, a concept that is used in the Gillian verification platform to automate
frame inference efficiently. We extract matching plans and their automation machinery from the
Gillian implementation and present them in a tool-agnostic way, making the Gillian approach
available to the broader verification community as a verification-tool design pattern.