Fundamentos del software UZ 2020

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

Actualmente, la celebración del curso está prevista del 7 al 11 de septiembre de 2020, de manera tanto presencial en Zaragoza como remota.

Puedes consultar la descripción del curso en la web de los cursos de verano y preinscribirte hasta el 31 de mayo rellenando el formulario de inscripción.

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

Noticias

  • 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

13 de julio

  • 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

14 de julio

  • 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

15 de julio

  • 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

16 de julio

  • 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

17 de julio

  • 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

Materiales

Disponibles próximamente.

Lugar de celebración

Disponible próximamente.

El curso se celebrará también de manera no presencial.

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 Instituto Max Planck para la Ciberseguridad y la Privacidad, 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.