Te damos la bienvenida a la página web del curso Fundamentos del software: introducción a la programación verificada y segura.
El curso se celebrará en julio de 2021.
- Noticias
- Presentación
- Requisitos e inscripción
- Programa
- Evaluación
- Materiales
- Lugar de celebración
- Espacios participativos
- Equipo docente
- Patrocinadores y ayudas
Noticias
-
3 de marzo de 2021
Confirmación de celebración del curso por la Universidad de Zaragoza.
-
17 de mayo de 2021
Apertura del plazo de inscripción.
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:
-
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.
-
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.
-
Estudiaremos los principales aspectos prácticos de programación segura a considerar en el desarrollo de cualquier sistema informático, así como las especificaciones que reflejan sus requisitos de seguridad.
A lo largo del curso, ilustraremos la utilidad práctica de sus contenidos por medio de casos de estudio de sistemas reales (sistemas operativos, compiladores, bases de datos, etc.) creados siguiendo esta metodología, así como las herramientas utilizadas para ello.
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 e inscripción
Información disponible próximamente.
Programa
Información disponible próximamente.
Evaluación
Información disponible próximamente.
Materiales
Información disponible próximamente.
Lugar de celebración
Información disponible próximamente.
Espacios participativos
Información disponible 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 el Max Planck Institute for Security and Privacy, y antes en la sede de París de Inria, centro de desarrollo del sistema Coq. 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.
Patrocinadores y ayudas
Información disponible próximamente.