Verification of algorithms in Escher

Abstract

This project borns from the growing need not only for quality programs but programs that never fail. Nowadays software is several orders of magnitude greater than just a few decades ago and critical software has become even more relevant, since if it fails, enormous, complex infrastructures fall with it, damaging machines, companies or even human lives. When software testing is not enough, it is imperative to use formal verification of algorithms and data structures. Since it is a meticulous, large task, we need computer-aided program verification to help us to speed up and get confidence on the process. This project aims to assay and understand a tool created for this purpose: Escher C Verifier, made for enabling the development of formally-verifiable sofware in a subset of C. By verifying some known algorithms, we want to study its aptness as an academic tool.

Este trabajo nace de la creciente necesidad no solo de programas de calidad, sino de programas que nunca fallen. Actualmente el software es varios órdenes de magnitud más grande que hace tan solo unas décadas y el software crítico se ha vuelto más importante aún, dado que si falla, enormes y complejas infraestructuras caen con él, dañando máquinas, empresas o incluso vidas humanas. Cuando el testing de software no es suficiente, es necesario emplear la verificación formal de algoritmos y estructuras de datos. Puesto que es una tarea meticulosa y extensa, requerimos de la verificación asistida de programas para ayudarnos a acelerar y ganar confianza en el proceso. Este proyecto apunta a analizar y comprender una herramienta creada para este propósito: Escher C Verifier, hecha para permitir el desarrollo de software formalmente verificable en un subconjunto de C. A partir de la verificación de algunos algoritmos conocidos, queremos estudiar su aptitud como una herramienta académica.