Verification of Greedy Algorithms in Dafny

Abstract

The proof that a program works according to a previously established behavior is known as formal verification. The use of formal verification techniques is increasing in recent years and in areas of the software industry. In this paper, the behavior of some greedy algorithms will be formally verified in Dafny. This will involve carrying out rigorous mathematical proofs in Dafny. In this paper, Dafny will be introduced first. It is a programming language that allows the user to check the correctness of his/her code. This will require a detailed specification of the expected behavior of the code. Secondly, greedy algorithms will be explained in detail, different problems where the greedy method is applied will be presented, and the strategy they follow to obtain an optimal solution will be studied. The specification of the code of each problem will be developed in Dafny and then the implementation of the greedy algorithm that solves it will be carried out in order to finally verify it. In addition, a generic methodology will be designed with the idea of being able to establish some steps to follow in the verification of these greedy algorithms for specific problems.

La demostración de que un programa funciona de acuerdo a un comportamiento previamente establecido es lo que se conoce como verificación formal. El empleo de técnicas de verificación formal está incrementándose en los últimos años y en áreas de la industria del software. En este trabajo, se verificará formalmente el comportamiento de algunos algoritmos voraces en Dafny. Esto implicará llevar a cabo demostraciones matemáticas rigurosas en Dafny. En el presente trabajo se introducirá Dafny en primer lugar. Es un lenguaje de programación que permite al usuario comprobar la corrección de su código. Para ello hará falta una especificación detallada del comportamiento esperado del código. En segundo lugar, se explicarán con detalle los algoritmos voraces, se presentarán diferentes problemas donde se aplica el método voraz y se estudiará la estrategia que siguen para obtener una solución óptima. Se desarrollará la especificación de cada problema en Dafny y posteriormente se llevar´a a cabo la implementación del algoritmo voraz que lo resuelve, para finalmente poder verificarlo. Además, se diseñaría una metología genérica con la idea de poder establecer unos pasos a seguir en la corrección de estos algoritmos voraces para ciertos problemas.