Fundamentos del software: introducción a la programación verificada

Fecha evento: 
07/09/2020 al 11/09/2020
Coordinadores: 

Roberto Blanco Martínez, Investigador en Inria Paris / MPI for Cyber Security and Privacy.
Ricardo J. Rodríguez Fernández, Profesor Ayudante Doctor de la Universidad de Zaragoza.

Online
Horas lectivas totales: 
50.00h.
Horas lectivas presenciales: 
30
Horas no presenciales: 
20.00h.
Tarifa general: 
160 euros
Tarifa reducida: 
130 euros
Inscripción cerrada
Objetivos: 

¿Es posible construir sistemas informáticos libres de errores? Lejos de ser una curiosidad filosófica, este curso da una respuesta matemáticamente rigurosa y afirmativa a esta pregunta fundamental y proporciona las herramientas para su puesta en práctica. La corrección de un programa se establece en base a una especificación: el programa es correcto si obedece su especificación. A lo largo del curso se aprenderán los fundamentos y lenguajes de programación que permiten, por una parte, expresar especificaciones de complejidad arbitraria como valores de primera clase del lenguaje, y, por otra, demostrar interactivamente que una implementación dada satisface la especificación asignada. Estas técnicas se aplicarán a la programación de algoritmos correctos por construcción en lenguajes de programación estándar, tanto funcionales como imperativos. La utilidad práctica de los contenidos del curso se ilustrará a través de casos de estudio de sistemas reales (sistemas operativos, compiladores, bases de datos, etc.) creados siguiendo esta metodología; adicionalmente, se estudiarán los principales aspectos prácticos de programación segura a considerar en el desarrollo de cualquier sistema informático. Las sesiones combinarán la exposición de conceptos con su puesta en práctica interactiva en Coq, seguida de y complementada por ejercicios con los que los participantes desarrollarán gradualmente su dominio del lenguaje, que culminará con la construcción de un pequeño sistema verificado.

Programa: 

Lunes, 7 de septiembre
09:00 h. Programas funcionales. Inducción estructural. Estructuras de datos: listas
11:00 h. Programación genérica: polimorfismo. Tácticas de demostración
14:00 h. Lógica computacional
16:00 h. Introducción a la programación segura: Motivación y estándares

Martes, 8 de septiembre
09:00 h. Proposiciones inductivas (1ª parte)
11:00 h. Proposiciones inductivas (2ª parte)
14:00 h. Diccionarios. Semántica de los lenguajes imperativos (1ª parte)
16:00 h. Programación segura: Lenguajes de programación. Lenguaje C

Miércoles, 9 de septiembre
09:00 h. Semántica de los lenguajes imperativos (2ª parte)
11:00 h. Automatización de demostraciones
14:00 h. Caso de estudio. Proyectos de curso
16:00 h. Programación segura: Cadenas. Enteros

Jueves, 10 de septiembre
09:00 h. Verificación funcional. Ordenación.
11:00 h. Árboles binarios. Encapsulación. Generación de código verificado.
14:00 h. Árboles rojinegros. Automatización práctica.
16:00 h. Programación segura: Salidas con formato. Condiciones de carrera.

Viernes, 11 de septiembre
09:00 h. Verificación imperativa. Lógica de Hoare (1ª parte).
11:00 h. Lógica de Hoare (2ª parte). Verificación del lenguaje C.
14:00 h. Estado del arte del software verificado.
16:00 h. Laboratorio de programación segura.

Ponentes: 

1 Ricardo J. Rodríguez Fernández, Profesor Ayudante Doctor de la Universidad de Zaragoza
2 Roberto Blanco Martínez, Starting Researcher, INRIA (Francia)

Alumnado: 

El curso puede interesar a ingenieros titulados, investigadores y otros profesionales de las tecnologías de la información, así como a estudiantes de doctorado, máster y cursos avanzados de grado, en particular en informática, matemáticas y disciplinas próximas.

Cada participante debe disponer de un ordenador para el seguimiento de las sesiones prácticas y el trabajo personal o en grupo alrededor de los ejercicios planteados. Los equipos deben poder ejecutar el software Coq, bien de forma nativa o en una máquina virtual con sistema operativo Linux, macOS o Windows, bien de forma embebida en un navegador web estándar.

Reconocimiento de créditos: 

Solicitado el reconocimiento como créditos por las Actividades universitarias culturales por la Universidad de Zaragoza.

1,5 ECTS

1. Los asistentes pueden solicitar individualmente a los Servicios Provinciales de Educación el reconocimiento de la actividad como Formación Permanente de Profesorado presentando el certificado de haber realizado el curso.

2. Reconocimiento como créditos ECTS en el Grupo 9 de Universidades (G-9): Más información en https://cursosextraordinarios.unizar.es/ (Apartado créditos).

3. Créditos ECTS en otras universidades.

Los estudiantes interesados en que su Universidad les reconozca como créditos ECTS por haber realizado un Curso de Verano de la Universidad de Zaragoza, deben consultar con la Secretaría de su Facultad o Escuela de origen tal posibilidad.

Procedimiento de evaluación: 

Realización de trabajos prácticos. Se prevén 10 horas de trabajos basados en las sesiones de cada día, a razón de 2 horas por día del curso, sumadas a otras 10 horas para el desarrollo y evaluación de un trabajo final de asignatura que consolida los conocimientos adquiridos.