Resumen:
Desde hace ya un buen número de años, existen diversas herramientas, altamente automatizadas e integradas en entornos de desarrollo, para la verificación de sistemas reales escritos en los principales lenguajes de programación. Estas herramientas ya se han utilizado con éxito, a nivel industrial, para desarrollar software fiable, especialmente software crítico. Concretamente, la verificación deductiva de software, que se inició en la década de 1960, ha tenido un largo camino, desde las pruebas en lápiz y papel, hasta las pruebas altamente automatizadas que se realizan hoy en día. Se puede decir que el área ha alcanzado una etapa de madurez que permite que la tecnología de verificación deductiva se haya expandido al entorno industrial. En esta charla ilustraremos el
estado del arte en esta área a través de la herramienta Dafny (desarrollada por Microsoft Research). Dafny es un lenguaje de programación (imperativo y funcional) diseñado con la verificación en mente y con un buen soporte para la especificación. Su compilador
incluye un verificador de programas que se ejecuta en segundo plano en el entorno de desarrollo. Dafny destaca por ofrecer una experiencia de verificación integrada y particularmente accesible que lo hace muy adecuado no sólo para la enseñanza del paradigma de la verificación deductiva como método de desarrollo de software fiable, sino también para la enseñanza de los conceptos básicos de programación. Dafny genera automáticamente código en varios lenguajes de uso común (e.g. C# y Java), pero también establece una excelente base para el aprendizaje de otras herramientas de verificación deductiva (e.g. Key y Spark) que se aplican directamente a lenguajes como Java, ADA o C++.