Validación Automática de Contratos Software con Z3

Abstract

[ES] En Ingeniería de Software, el concepto de contrato está relacionado con una especificación del comportamiento de los programas utilizando descripciones que típicamente incluyen precondiciones y postcondiciones. El estado del arte actual permite generar automáticamente contratos a partir del código fuente que pueden ser usados como entrada para analizadores cada vez más potentes. Sin embargo, los contratos generados automáticamente pueden no ser completamente precisos o correctos, conteniendo algunos elementos que no están verificados. El objetivo de este proyecto es desarrollar una aplicación que permite refinar dichos contratos, utilizando el sistema resolutor SMT Z3 para identificar y eliminar aquellos componentes que el proceso de validación determina que son demostradamente falsos.

[EN] Software contracts provide formal specification for the terms of the service that software components can provide. Contracts on software are essentially written by using program preconditions and postconditions that formalize the mutual obligations and benefits of the software units or routines. The current state of the art allows contracts to be automatically inferred from the source code so that can be used as input for increasingly powerful analyzers. However, automatically generated contracts can not be completely accurate or correct, containing some elements that are not verified. The goal of this project is to develop a software application that allows contracts to be refined by using the SMT solver Z3 to identify and eliminate those components that are proved to be false.

[CA] En Enginyeria de Software, el concepte de contracte està relacionat amb una especificació del comportament dels programes utilitzant descripcions que típicament inclouen precondicions i postcondicions. L’estat de l’art actual permet generar automàticament contractes a partir de el codi font que poden ser usats com a entrada per a analitzadors cada vegada més potents. No obstant això, els contractes generats automàticament poden no ser completament precisos o correctes, contenint alguns elements que no estan verificats. L’objectiu d’aquest projecte és desenvolupar una aplicació que permet refinar aquests contractes, utilitzant el sistema resolutori SMT Z3 per identificar i eliminar aquells components que el procés de validació determina que són demostradament falsos.