Linhas de Produtos de Software exploram reuso entre sistemas de software, fornecendo uma maneira sistemática de gerá-los. Extrair e evoluir linhas de produtos a partir de produtos existentes pode ser caro e propenso a erros. Tais tarefas podem se beneficiar de refatoramentos com base formal, garantindo corretude por construção. Linhas de produtos são muitas vezes desenvolvidas no contexto de um conjunto de linhas relacionadas. Por exemplo, no contexto de populações de produtos, podemos ter diferentes versões de uma linha sendo desenvolvidas simultaneamente em diferentes branches. Também podemos combinar várias linhas que dependem umas das outras para desenvolver multilinhas de produto. Ao evoluir uma linha pertencente a um conjunto, é importante verificar se as alterações afetam as demais linhas do mesmo conjunto. A teoria de refinamento de linhas de produtos formaliza a noção de evolução segura em termos de uma relação de refinamento. Refinamento captura preservação de comportamento, mas abstrai melhoria de qualidade. Neste trabalho, n´os estendemos essa teoria para populações de produtos e multilinhas de produtos. Estabelecemos propriedades de composicionalidade, que estabelecem as condições necessárias para garantir a evolução segura de conjuntos de linhas quando evoluímos individualmente seus membros. As teorias de refinamento são gerais com respeito às diferentes linguagens usadas para descrever modelos de características, modelos de configuração e demais artefatos para implementar linhas de produtos e conjuntos de linhas. Pressupostos e axiomas estabelecem as interfaces entre nossas teorias e linguagens específicas. Instanciar as teorias com diferentes combinações de linguagens concretas nos permite derivar transformações que abstraem evoluções seguras, que vão desde a evolução individual de artefatos até a evolução de linhas de produtos e seus conjuntos como um todo. Investigamos e exploramos semelhanças entre estas linguagens, abstraindo propriedades em comum, o que resulta em transformações expressas em n´níveis mais altos de abstração, que podem ser reutilizados por mais linguagens. Desta forma, n´os propomos uma linha de produtos de teorias, onde diferentes linguagens correspondem a diferentes features, e os produtos correspondem à instanciações das teorias de refinamento. Foi utilizado o Prototype Verification System para codificação e prova das teorias e suas instanciações. Para avaliar a expressividade das transformações propostas, analisamos o histórico de evolução de linhas de produtos, observando se transformações são expressivas o suficiente para justificar os cenários de evolução segura. Além disso, também estudamos a evolução do kernel do Linux e mostramos que a maioria dos padrões de evolução encontrados está de acordo com a noção de refinamento de linhas de produtos. Finalmente, também usamos as transformações para raciocinar sobre a evolução da linha de produtos de teorias.CNPqSoftware Product Lines explore reuse among software systems, providing a systematic way to generate them. Extracting product lines from existing products and evolving them can be costly and error-prone. These tasks can benefit from refactorings with formal basis, to ensure correctness by construction. Product lines are often developed in the context of a set of related product lines. In the context of product populations, we might have a number of product line versions being simultaneously developed in different branches. We can also combine multiple product lines that depend on each other to develop multi product lines. When evolving a product line from such a set, it is important to check whether the changes affect the related product lines in the same set. A theory of product line refinement formalizes the notion of safe evolution in terms of a refinement relation over product lines. Refinement captures behavior preservation but abstracts quality improvement. In this work, we extend this theory, defining refinement theories for product populations and multi product lines. We also establish compositionality properties, which reveal the necessary conditions for guaranteeing safe evolution of sets of product lines when individually evolving one of its members. The refinement theories are generic with respect to the different feature model, configuration knowledge, and asset languages that we can use to describe or implement product lines, and consequently, sets of product lines. Assumptions and axioms explicitly establish the interfaces between our theories and particular languages. Instantiating the theories with different combinations of concrete languages enables us to derive refinement templates that abstract safe evolution transformations, ranging from evolving individual artifacts to evolving product lines and their sets as a whole. We investigate and explore similarities between these languages, abstracting common properties, which ultimately result on refinement templates that work at a higher abstraction level and can be reused to a larger number of languages. Thus, we propose a product line of theories, where different languages correspond to different features, and products correspond to instantiations of the refinement theories. We use the Prototype Verification System to encode and prove soundness of the theories and their instantiations. To evaluate expressiveness of the proposed templates, we analyze the evolution history of product lines. We observe whether templates are expressive enough to address the safe evolution scenarios. Additionally, we also study the Linux kernel evolution and discover that most evolution patterns conform to the product line refinement notion. Finally, we also use refinement templates to reason about evolution of the product line of theories.