Ciencias de la Computación (plan 2013) 2021-2

Optativas, Seminario de Ciencias de la Computación B

Verificación formal de software.

URL de la clase: Verificación formal de Software (seminario de CC B) meet.google.com/vwb-kjye-imm
(Esta url permanece mientras no se avise lo contrario, por este medio o mediante la lista de correo del grupo)

Descripción del curso.

Este curso es una introducción a la verificación formal de modelos de software.
El curso está dirigido a estudiantes de Computación y estudiantes de Matemáticas.

El curso comienza con un panorama sobre la necesidad de verificación formal de sistemas
destacando dos enfoques complementarios: verificación de modelos y deducción automática.
Posteriormente, se introduce el tema de Lógica temporal y su aplicación en verificación formal.
Finalmente, considerando que el uso de abstracción es una idea crucial en el razonamiento sobre programas,
se presenta el tema de Abstracción de Predicados con ejemplos de su aplicación.
El desarrollo del curso intercala la exposición de fundamentos teóricos con la aplicación básica
de algunas herramientas de verificación formal.

Miguel Carrillo. Publicaciones según Google Scholar.

Preguntas o comentarios sobre este curso: miguel.mcb@gmail.com

Método de Trabajo y Forma de Evaluación.

El curso se impartirá en forma autocontenida (aunque es recomendable haber aprobado Lógica Computacional, o Lógica Matemática I). Es ideal, no indispensable, tener conocimientos básicos de Lógica Temporal (Lógicas no clásicas).

Para mantener comunicación, los interesados en el curso deben registrarse en el grupo de Verificacion Formal de Software.

Temario.

1. Antecedentes y motivación

• 1.1 Errores en sistemas
• 1.2 Pruebas de software (Software testing)
• 1.3 Soluciones no formales y/o no automatizadas

2. Enfoques de verificación formal automatizada

• 2.1 Lenguajes de especificación, Modelos, y Teorías.
• 2.2 Verificación de modelos
• 2.3 Deducción automática

3. Lenguajes de especificación

• 3.1 Lógica de tiempo lineal (LTL)
• 3.2 Lógica de árboles de cómputo (CTL)
• 3.3 Variantes de Lógica de predicados
• 3.3 Semántica. Modelos (sistemas de transición de estados)

4. Verificación de modelos

• 4.1 Modelado de programas
• 4.2 Expresión de propiedades

5. Técnicas de verificación

• 5.1 Verificación simbólica
• 5.2 Verificación acotada

6. Abstracción de predicados

• 6.1 Abstracción existencial
• 6.2 Programas Booleanos

7. Uso básico de algunas herramientas para verificación de programas (NuXmv,Alloy,SatAbs,CBMC).
Este tema se intercala con los demás temas a lo largo del curso.

Referencias.
1. Clarke, Edmund M., et al., eds. Handbook of model checking. Springer, 2018.
2. Clarke Jr, Edmund, Orna Grumberg, Daniel Kroening, Doron Peled, Helmut Veith. Model checking. MIT press, 2018.
3. Huth, Ryan. Logic in Computer Science: Modelling and reasoning about systems. Cambridge university press, 2004.
4. Bozzano, Marco, et al. nuXmv 2.0 User Manual. Fondazione Bruno Kessler, Tech. Rept., 2019.
5. Jackson, Daniel. Software Abstractions: logic, language, and analysis. MIT press, 2012.
6. Clarke, Kroening, Lerda. A tool for checking ANSI-C programs.TACAS 2004.
7. Kroening, Daniel. The CProver User Manual. http://www.cprover.org/cprover-manual/, Último acceso 2021.
8. Kroening, Daniel. SATABS Predicate Abstraction using SAT. http://www.cprover.org/satabs/, Último acceso 2021.