Fundamentos del software UZ 2020

Te damos la bienvenida a la página web de Fundamentos del software: introducción a la programación verificada.

Presentación

¿Es posible construir sistemas informáticos libres de errores? Lejos de ser una pura curiosidad académica, este curso da una respuesta afirmativa y matemáticamente rigurosa a esta pregunta fundamental y proporciona las herramientas necesarias para su puesta en práctica.

La corrección de un programa se establece en base a una especificación: un programa que lleva asociada una especificación es correcto con respecto a la misma si y solo si obedece dicha especificación. A lo largo del curso:

  1. Aprenderemos los fundamentos y lenguajes de programación que permiten, por una parte, expresar especificaciones como valores de primera clase del lenguaje, y, por otra, demostrar interactivamente que una implementación dada satisface su especificación correspondiente.

  2. Aplicaremos estas técnicas a la programación de algoritmos correctos por construcción en lenguajes de programación estándar, tanto funcionales como imperativos.

  3. Ilustraremos la utilidad práctica de los contenidos del curso a través de casos de estudio de sistemas reales (sistemas operativos, compiladores, bases de datos, etc.) creados siguiendo esta metodología. Además, estudiaremos los principales aspectos prácticos de programación segura a considerar en el desarrollo de cualquier sistema informático.

Las sesiones de trabajo combinan la exposición aplicada de conceptos con su puesta en práctica interactiva, complementada por ejercicios con los que los participantes desarrollarán gradualmente su dominio de las herramientas de desarrollo, que culminarán en la construcción de un pequeño sistema verificado.

Requisitos

El curso es accesible a cualquier persona con conocimientos de lenguajes de programación y fundamentos matemáticos comparables a los de un segundo curso de grado en ingeniería informática, matemáticas y planes de estudios relacionados, o experiencia asimilable.

Puede ser especialmente interesante para ingenieros titulados, investigadores y profesionales de las tecnologías de la información, así como para estudiantes de doctorado, máster y cursos avanzados de grado, en particular en informática, matemáticas y disciplinas próximas.

Programa

Día 1

  • Sesión 1: Programas funcionales. Inducción estructural. Estructuras de datos: listas

  • Sesión 2: Programación genérica: polimorfismo. Tácticas de demostración

  • Sesión 3: Lógica computacional

  • Sesión 4: Introducción a la programación segura: Motivación y estándares

Día 2

  • Sesión 1: Proposiciones inductivas (1ª parte)

  • Sesión 2: Proposiciones inductivas (2ª parte)

  • Sesión 3: Diccionarios. Semántica de los lenguajes imperativos (1ª parte)

  • Sesión 4: Programación segura: Lenguajes de programación. Lenguaje C

Día 3

  • Sesión 1: Semántica de los lenguajes imperativos (2ª parte)

  • Sesión 2: Automatización de demostraciones

  • Sesión 3: Caso de estudio. Proyectos de curso

  • Sesión 4: Programación segura: Cadenas. Enteros

Día 4

  • Sesión 1: Verificación funcional. Ordenación

  • Sesión 2: Árboles binarios. Encapsulación. Generación de código verificado

  • Sesión 3: Árboles rojinegros. Automatización práctica

  • Sesión 4: Programación segura: Salidas con formato. Condiciones de carrera

Día 5

  • Sesión 1: Verificación imperativa. Lógica de Hoare (1ª parte)

  • Sesión 2: Lógica de Hoare (2ª parte). Verificación del lenguaje C

  • Sesión 3: Estado del arte del software verificado

  • Sesión 4: Laboratorio de programación segura

Lugar de celebración

Materiales

Disponibles próximamente.

Equipo docente

Roberto Blanco es ingeniero en informática por la Universidad de Zaragoza y doctor en informática por la École polytechnique/Université Paris-Saclay, e investigador en la sede de París de Inria, centro de desarrollo del sistema Coq, y próximamente en el Instituto Max Planck para la Ciberseguridad y la Privacidad. Su trabajo gira en torno al desarrollo de métodos formales y su aplicación a la verificación de sistemas informáticos y de su seguridad, concentrado en la actualidad en la compilación segura.

Ricardo J. Rodríguez es ingeniero en informática por la Universidad de Zaragoza y doctor en informática por la misma universidad. Actualmente es profesor en la Escuela de Ingeniería y Arquitectura de la Universidad de Zaragoza, donde realiza tareas docentes y de investigación. Su trabajo de investigación gira en torno al análisis de propiedades de sistemas como rendimiento, seguridad y dependability.