Verificación Formal de Programas
Análisis de flujo de datos
Análisis de flujo de información
Seguimiento de flujos de datos sensibles
Identificación de filtraciones de información
Análisis de propagación de información
Análisis de flujo de control
Optimización de la estructura de control
Identificación de cuellos de botella
Análisis de rutas críticas
Análisis de dependencias
Resolución de dependencias circulares
Detección de ciclos de datos
Análisis de dependencia de datos
Garantías de calidad en software
Mejora continua del software
Recopilación de comentarios
Encuestas de satisfacción
Retroalimentación del usuario
Análisis estático de código
Revisión de código
Análisis de calidad de código
Análisis de código fuente
Pruebas de software
Pruebas de aceptación del usuario
Pruebas de integración
Pruebas funcionales
Modelado de sistemas
Verificación de concurrencia
Gestión de exclusión mutua
Detección de condiciones de carrera
Control de concurrencia
Verificación de rendimiento
Evaluación tiempo de ejecución
Análisis de uso de memoria
Optimización de recursos
Verificación de propiedades de sistemas
Auditoría de acceso
Análisis de vulnerabilidades
Seguridad y privacidad
Análisis de Algoritmos
Notación Asintótica
Eficiencia de un algoritmo
Tasa de crecimiento
Notación O (n²)
Notación Ω (n)
Notación Θ (n log n)
Tasa de Crecimiento de T(n)
Funciones lineales Cuadráticas y Exponenciales
Función de Tiempo respecto a n
Complejidad Computacional de Algoritmos
Memoria Utilizada
Tiempo de Ejecución
Mejor Caso y Peor Caso
Escenarios óptimos y pesimistas
Ordenamiento de burbuja
Estimación de Tiempo de Ejecución
Operaciones básicas de un algoritmo
Algoritmo de ordenamiento
Lógica de Hoare
Triplas de Hoare
Formato: {P} S {Q}
{P}Precondición
{S}Instrucción
{Q}Postcondición
Verificación de Programas Iterativos
Cota de Ciclo
Asegura que el ciclo terminará
Invariante de Bucle
Condición que es verdadera antes y después de cada iteración del bucle
Verificación de la Corrección de Programas
Pruebas formales
Pruebas de ejecución
Corrección Parcial
Corrección Total
Tipos de Instrucciones y sus Verificaciones
Composición Secuencial
Precondición más débil (wp): wp(S1, wp(S2, R))
Ejecuta instrucciones una tras otra.
Instrucción Condicional
Precondición más débil (wp): (C ⇒ wp(A, R)) ∧ (¬C ⇒ wp(B, R))
Ejecuta diferentes caminos de código según una condición.
Asignación
Precondición más débil (wp): R(x:=E) donde x es la variable y E la expresión.
Cambia el valor de una variable.
Instrucción Vacía
Precondición más débil (wp): Es igual a la poscondición.
No modifica el estado del programa.
