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

El curso se celebró del 7 al 11 de septiembre de 2020 de manera remota.

Puedes consultar la descripción del curso en la web de los cursos de verano.

Ante cualquier pregunta, no dudes en contactar con los directores del curso.

• Noticias
• Presentación
• Requisitos e inscripción
• Programa
• Evaluación
• Materiales
• Lugar de celebración
• Espacios participativos
• Equipo docente
• Patrocinadores y ayudas

Noticias

• 30 de septiembre de 2020

  Finalización de los trabajos de curso. ¡Gracias por vuestra participación!

• 25 de septiembre de 2020

  Extensión de la fecha de entrega de los trabajos de curso hasta el 30 de septiembre.

• 14 de septiembre de 2020

  Fijada fecha límite de entrega de los trabajos de curso el 27 de septiembre.

• 11 de septiembre de 2020

  Clausura del curso.

• 7 de septiembre de 2020

  Comienzo del curso.

• 14 de julio de 2020

  Confirmación de nuevas fechas de celebración del 7 al 11 de septiembre.

• 7 de julio de 2020

  Celebración del curso postpuesta a septiembre.

• 10 de junio de 2020

  Confirmación definitiva de realización del curso por parte de la Universidad de Zaragoza. Comienzo del periodo de matrícula.

• 31 de mayo de 2020

  Cierre de el periodo de preinscripción. Se siguen aceptando nuevas inscripciones.

• 14 de mayo de 2020

  Aprobación de la opción de participación remota por la Universidad de Zaragoza.

• 3 de mayo de 2020

  Aprobación de patrocinio por parte de CPIIAR y AI2Aragón con tarifas reducidas para sus miembros.

• 27 de abril de 2020

  Publicación de los cursos de verano y apertura del periodo de preinscripción y solicitud de informació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:

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 e inscripción

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.

Las preinscripciones y solicitudes de información se realizan a través de este formulario. La Universidad de Zaragoza evaluará las posibilidades de celebración del curso, lugares y fechas en función del número de inscritos en la primera semana de junio y las condiciones sanitarias. Por ello, animamos a los interesados a completar la solicitud durante el mes de mayo.

La celebración del curso está prevista en un formato mixto que combine participación remota y presencial, en caso de que esta última sea posible.

Programa

7 de septiembre

• 09.00-10.30: Programas funcionales. Inducción estructural. Estructuras de datos: listas

• 11.00-12:30: Programación genérica: polimorfismo. Tácticas de demostración

• 14.00-15.30: Lógica computacional

• 16.00-17.30: Introducción a la programación segura: Motivación y estándares

8 de septiembre

• 09.00-10.30: Proposiciones inductivas (1ª parte)

• 11.00-12:30: Proposiciones inductivas (2ª parte)

• 14.00-15.30: Diccionarios. Semántica de los lenguajes imperativos (1ª parte)

• 16.00-17.30: Programación segura: Lenguajes de programación. Lenguaje C

9 de septiembre

• 09.00-10.30: Semántica de los lenguajes imperativos (2ª parte)

• 11.00-12:30: Automatización de demostraciones

• 14.00-15.30: Caso de estudio. Proyectos de curso

• 16.00-17.30: Programación segura: Cadenas. Enteros

10 de septiembre

• 09.00-10.30: Verificación funcional. Ordenación

• 11.00-12:30: Árboles binarios. Encapsulación. Generación de código verificado

• 14.00-15.30: Árboles rojinegros. Automatización práctica

• 16.00-17.30: Programación segura: Salidas con formato. Condiciones de carrera

11 de septiembre

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

• 11.00-12:30: Lógica de Hoare (2ª parte). Verificación del lenguaje C

• 14.00-15.30: Estado del arte del software verificado

• 16.00-17.30: Laboratorio de programación segura

Evaluación

La organización de los cursos de verano expedirá un diploma de participación a todos aquellos que asistan al menos al 85% de las sesiones del curso, que totalizan 30 horas lectivas sumadas a 10 horas de trabajo personal en los ejercicios asignados.

La superación formal del curso conlleva la obtención de 1,5 créditos ECTS. Los participantes interesados en esta modalidad de evaluación deberán coordinar con los profesores la realización y exposición de un trabajo de profundicación sobre alguna de las partes del curso de unas 10 horas adicionales.

Materiales

Disponibles en el repositorio del curso.

Lugar de celebración

El curso se celebrará exclusivamente de manera no presencial a través de un canal disponible a los participantes.

Espacios participativos

El chat Zulip del curso es el canal de comunicación principal entre todos los participantes.

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

El Colegio Profesional de Ingenieros en Informática de Aragón y la Asociación de Ingenieros en Informática de Aragón subvencionarán la participación en el curso a sus miembros reembolsándoles la diferencia entre la tarifa general y la tarifa reducida, de forma que puedan disfrutar de esta última incluso si no satisfacen los criterios propios de la Universidad de Zaragoza.