Verificación Formal de Programas

Tipos de Instrucciones y sus Verificaciones

Instrucción Vacía

No modifica el estado del programa.

Precondición más débil (wp): Es igual a la poscondición.

Asignación

Cambia el valor de una variable.

Precondición más débil (wp): R(x:=E) donde x es la variable y E la expresión.

Instrucción Condicional

Ejecuta diferentes caminos de código según una condición.

Precondición más débil (wp): (C ⇒ wp(A, R)) ∧ (¬C ⇒ wp(B, R))

Composición Secuencial

Ejecuta instrucciones una tras otra.

Precondición más débil (wp): wp(S1, wp(S2, R))

Lógica de Hoare

Verificación de la Corrección de Programas

Corrección Parcial
Corrección Total

Pruebas formales
Pruebas de ejecución

Verificación de Programas Iterativos

Invariante de Bucle

Condición que es verdadera antes y después de cada iteración del bucle

Cota de Ciclo

Asegura que el ciclo terminará

Triplas de Hoare

{P}Precondición
{S}Instrucción
{Q}Postcondición

Formato: {P} S {Q}

Análisis de Algoritmos

Estimación de Tiempo de Ejecución

Operaciones básicas de un algoritmo

Algoritmo de ordenamiento

Mejor Caso y Peor Caso

Ordenamiento de burbuja

Escenarios óptimos y pesimistas

Complejidad Computacional de Algoritmos

Tiempo de Ejecución

Memoria Utilizada

Tasa de Crecimiento de T(n)

Función de Tiempo respecto a n

Funciones lineales Cuadráticas y Exponenciales

Notación Asintótica

Notación O (n²)
Notación Ω (n)
Notación Θ (n log n)

Tasa de crecimiento

Eficiencia de un algoritmo

Modelado de sistemas

Verificación de propiedades de sistemas

Seguridad y privacidad

Análisis de vulnerabilidades

Auditoría de acceso

Verificación de rendimiento

Optimización de recursos

Análisis de uso de memoria

Evaluación tiempo de ejecución

Verificación de concurrencia

Control de concurrencia

Detección de condiciones de carrera

Gestión de exclusión mutua

Garantías de calidad en software

Pruebas de software

Pruebas funcionales

Pruebas de integración

Pruebas de aceptación del usuario

Análisis estático de código

Análisis de código fuente

Análisis de calidad de código

Revisión de código

Mejora continua del software

Retroalimentación del usuario

Encuestas de satisfacción

Recopilación de comentarios

Análisis de flujo de datos

Análisis de dependencias

Análisis de dependencia de datos

Detección de ciclos de datos

Resolución de dependencias circulares

Análisis de flujo de control

Análisis de rutas críticas

Identificación de cuellos de botella

Optimización de la estructura de control

Análisis de flujo de información

Análisis de propagación de información

Identificación de filtraciones de información

Seguimiento de flujos de datos sensibles