Verificación de algoritmos sobre segmentos de un vector utilizando módulos abstractos en Dafny

Abstract

La verificación formal de programas permite expresar y comprobar las propiedades que cumplen los programas. El objetivo de este proyecto es el de verificar algoritmos que computan información sobre los segmentos de un vector, como por ejemplo el segmento más largo que cumple una propiedad o el número de segmentos que cumple una propiedad. En primer lugar, se introducirá la herramienta Dafny, un lenguaje de programación que utiliza un resolutor SMT para comprobar las condiciones de verificación necesarias introducidas por el usuario. En segundo lugar, se llevará a cabo una explicación de los algoritmos con los que vamos a trabajar y algunos ejemplos concretos de su aplicación. Posteriormente, se modelizarán este tipo de problemas en Dafny, para poder así llevar a cabo la implementación del algoritmo en la herramienta, con el fin de finalmente verificar que cumple las propiedades que esperamos de las soluciones. Se tratará de presentar cada problema con diferentes niveles de abstracción, es decir, para cada problema se presentarán diferentes soluciones dependiendo del tipo de propiedades que se estén comprobando sobre los segmentos. De esta forma, para determinados casos obtendremos soluciones más eficientes.