IIC3800 - Tópicos en Ciencia de la Computación
Transparencias de Clases
Introducción a la verificación formal
[
versión con animaciones
|
versión para imprimir
]
Modelación de software usando autómatas
[
versión con animaciones
|
versión para imprimir
]
Introducción a las lógicas temporales
[
versión con animaciones
|
versión para imprimir
]
Expresividad de las lógicas temporales
[
versión con animaciones
|
versión para imprimir
]
Algoritmo de verificación para CTL
[
versión con animaciones
|
versión para imprimir
]
Autómatas sobre palabras infinitas: Parte I
[
versión con animaciones
|
versión para imprimir
]
Autómatas sobre palabras infinitas: Parte II
[
versión con animaciones
|
versión para imprimir
]
Autómatas sobre palabras infinitas: Construcción de Safra
[
versión con animaciones
|
versión para imprimir
]
Autómatas sobre palabras infinitas: Autómata y verificación de LTL (parte I)
[
versión con animaciones
|
versión para imprimir
]
Autómatas sobre palabras infinitas: Autómata y verificación de LTL (parte II)
[
versión con animaciones
|
versión para imprimir
]
Algoritmos de verificación para LTL y CTL
*
(parte I)
[
versión con animaciones
|
versión para imprimir
]
Algoritmos de verificación para LTL y CTL
*
(parte II)
[
versión con animaciones
|
versión para imprimir
]
Algoritmos de verificación para LTL y CTL
*
(parte III)
[
versión con animaciones
|
versión para imprimir
]
Operadores de punto fijo y el mu-calculus
[
versión con animaciones
|
versión para imprimir
]
Expresividad del mu-calculus
[
versión con animaciones
|
versión para imprimir
]
Verificación del mu-calculus
[
versión con animaciones
|
versión para imprimir
]