Partial evaluation (PE) is a branch of computer science that achieves code optimization via specialization. This article describes a PE methodology for optimizing rewrite theories that encode concurrent as well as nondeterministic systems by means of the Maude language. The main advantages of the proposed methodology can be summarized as follows: • An automatic program optimization technique for rewrite theories featuring several PE criteria that support the specialization of a broad class of rewrite theories. • An incremental partial evaluation modality that allows the key specialization components to be encapsulated at the desired granularity level to facilitate progressive refinements of the specialization. • All executability theory requirements are preserved by the PE transformation. Also the transformation ensures the semantic equivalence between the original rewrite theory and the specialized theory under rather mild conditions.
