Pereira, MárioNini, João Francisco Serrenho2026-04-292026-04-292025-12-16http://hdl.handle.net/10362/202681Ensuring that a program functions as intended is a complex issue that has been approached many times and in various ways throughout history. Human-assisted software verification is the most complete and reliable method, despite its inherent additional effort. The objective of this work is to ease proofs of complex programs by taking advantage of a relation to an equivalent program that is easier to prove. If it is possible to establish that two different programs are equivalent, it is also very likely that reusing the simplest specification will lead to a faster and easier proof of the more sophisticated program. Relational Hoare Logic paved the way to the development of several techniques to reason about the similarities of two different programs. In this work, we will base our approach on the concept of product programs to reduce relational verification into standard verification. Furthermore, there will be a description of the relevant background in order to effectively comprehend the approach we chose, as well as a presentation of the other possible methods to achieve what we propose. Finally, we describe the details of our implementation and showcase the capabilities of our tool using several real-world examples.Garantir que um programa se comporta como esperado é um assunto complexo que tem sido alvo de muitas e diferentes tentativas ao longo da história. A verificação de software assistida por humanos é o método mais confiável e completo, apesar do seu inerente esforço adicional. O objetivo deste trabalho é facilitar as provas de programas complexos a partir da relação entre este e um equivalente que seja mais simples de provar. Se for possível estabelecer que dois programas diferentes são equivalentes, então é altamente provável que reutilizar a especificação do mais simples levará a uma prova mais fácil e rápida do programa mais sofisticado. A lógica de Hoare relacional abriu caminho para o desenvolvimento de várias técnicas para raciocinar sobre as similaridades de dois programas diferentes. Neste trabalho, vamos basear a nossa abordagem no conceito de product programs para reduzir a verificação relacional a verificação "tradicional". Além disso, haverá uma descrição do conhecimento prévio necessário para compreender efetivamente a nossa abordagem, tal como a apresentação de outros possíveis métodos para alcançar aquilo a que nos propomos. Finalmente, descreveremos os detalhes da nossa implementação e demonstraremos as capacidades da nossa ferramenta através de diversos exemplos realistas.engDeductive verificationProgram equivalenceOCamlCameleerRelational Hoare logicProduct programsmaster thesis