Seminario:
Herramientas automáticas de verificación deductiva y desarrollo de software fiable

Fecha

2022-07-13

Editor

Sistedes

Publicado en

Seminarios Sistedes

Licencia

CC BY-NC-ND 4.0

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++.

Descripción

Acerca de Lucio, Paqui

Paqui Lucio es doctora en Matemáticas (UCM) desde 1994. Como profesora en la Universidad del País Vasco, desde 1982, ha impartido una gran variedad de asignaturas en todos los ciclos formativos de la Facultad de Informática de San Sebastián. Su trabajo investigador ha estado siempre centrado en la lógica matemática y sus aplicaciones en temas relacionados con el software y la inteligencia artificial. Desde 2007, lidera el grupo de investigación LoRea (Logic and Reasoning) dedicado a la lógica, el razonamiento automático, y a sus aplicaciones en diversas áreas de la Informática, en particular en la verificación de programas y de sistemas reactivos. Ha dirigido una tesis doctoral europea (2008) y otra tesis doctoral internacional (2012) que fue premio extraordinario de doctorado. Ha participado en 17 proyectos financiados por entidades públicas, siendo la investigadora principal en 4 proyectos nacionales y 6 autonómicos. Cuenta con 4 sexenios reconocidos por la CNEAI.

Palabras clave

Página completa del ítem
Notificar un error en este seminario
Mostrar cita
Mostrar cita en BibTeX
Descargar cita en BibTeX