Segura Díaz, Clara MaríaBlázquez Saborido, JorgeEl Kasouari Qessouri, Salma2025-09-112025-09-112025https://hdl.handle.net/20.500.14352/123856Formal verification is a technique that allows us to demonstrate, through mathematical methods, that a program meets its specification (the expected behavior of the program). Unlike traditional testing, it is not based on specific test cases, but on logical reasoning that guarantees the correctness of the code in all possible cases. In this work, we will develop a methodology to specify and verify backtracking algorithms in Dafny. This methodology is applied to two representative examples of problems solved by this algorithmic method. In this work we have used Dafny tool, a programming language designed for formal specification and assisted program verification. We will present the essential elements of the methodology using the knapsack problem as an example. In this problem, the search space is structured as a binary tree, which translates into recursively invoking the algorithm at most twice (a fixed amount). Then we will extend the methodology to specify and verify problems in which the search space is structured as an n-ary tree, which involves a loop of recursive invocations where the number of iterations depends on one of the problem’s dimensions. Specifically, we will verify the assigning tasks to employees problem. We will complete the methodology by introducing optimal bounds to reduce the search space and we will provide several bounds in both application examples. Finally, we will present conclusions and possible lines for future work.La verificación formal es una técnica que permite demostrar, mediante métodos matemáticos, que un programa cumple su especificación (el comportamiento esperado del programa). A diferencia de las pruebas tradicionales, no se basa en casos de prueba concretos, sino en razonamientos lógicos que garantizan la corrección del código en todos los casos posibles. En este trabajo desarrollaremos una metodología para especificar y verificar en Dafny algoritmos de vuelta atrás. Dicha metodología se aplica a dos ejemplos representativos de los problemas resueltos mediante este método algorítmico. En este trabajo hemos usado la herramienta Dafny, un lenguaje de programación diseñado para la especificación formal y la verificación asistida de programas. Se presentarán los elementos esenciales de la metodología utilizando como ejemplo el problema de la mochila. En dicho problema el espacio de búsqueda está estructurado como un árbol binario, lo que se traduce en invocar recursivamente al propio algoritmo dos veces a lo sumo (una cantidad fija). A continuación, extenderemos la metodología para especificar y verificar problemas en los que el espacio de búsqueda está estructurado como un árbol n-ario, lo cual implica un bucle de invocaciones recursivas donde el número de iteraciones depende de una de las dimensiones del problema. Concretamente, verificaremos el problema de asignar tareas a funcionarios. Completaremos la metodología introduciendo podas de optimalidad para reducir el espacio de búsqueda y proporcionaremos varias podas en ambos ejemplos de aplicación. Finalmente, se proporcionarán conclusiones y posibles líneas del trabajo futuro.spaAttribution-NonCommercial-NoDerivatives 4.0 Internationalhttp://creativecommons.org/licenses/by-nc-nd/4.0/bachelor thesisopen access004(043.3)DafnyVerificaciónVuelta atrásEspecificaciónPodaVerificationBacktrackingSpecificationBoundInformática (Informática)33 Ciencias Tecnológicas