RT Generic
T1 Verificación de algoritmos sobre segmentos de un vector utilizando módulos abstractos en Dafny
T2 Verification of algorithms on array slices using abstract modules in Dafny
A1 Martín Viñuelas, Pablo
AB 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.
YR 2024
FD 2024
LK https://hdl.handle.net/20.500.14352/106903
UL https://hdl.handle.net/20.500.14352/106903
LA spa
NO Trabajo de Fin Doble Grado en Matemáticas e Ingeniería Informática, Facultad de Informática UCM, Departamento de Sistemas Informáticos y Computación, Curso 2023/2024
DS Docta Complutense
RD 6 abr 2025