Projecte realitzat en col·laboració amb l'Institut de Recherche en Informatique de Toulouse i ONERA The French Aeroespace Lab

[ANGLÈS] Given the background in software and hardware evolution over the years as well as the demand of accurate information in different industrial areas as aeronautics, nuclear and medical is how this Master thesis born. Having as main objective helping to discharging complex proof obligations by combining two formal methods (Abstract Interpretation and Weakest Precondition) to improve the precision in the software analysis.

[CASTELLÀ] Teniendo en cuenta el fondo en la evolución del software y hardware en los últimos años, así como la demanda de información precisa en diferentes áreas industriales como la aeronáutico, nuclear y médica es cómo esta tesis de maestría ha nacido. Teniendo como objetivo principal contribuir a la ejecución de obligaciones complejas a prueba mediante la combinación de dos métodos formales (interpretación abstracta y pre condición más débil) para mejorar la precisión en el análisis de software.

[CATALÀ] Tenint en compte el fons en l'evolució del programari i maquinari en els últims anys, així com la demanda d'informació precisa en vaig diferents àrees industrials com l'aeronàutic, nuclear i mèdica és com aquesta tesi de mestratge nascut. Tenint com a objectiu principal contribuir a l'execució d'obligacions complexes a prova mitjançant la combinació de dos mètodes formals (interpretació abstracta i més feble condició prèvia) per millorar la precisió en l'anàlisi de programari.