Director
Camilo Rocha Niño

Estudiantes
ROMERO GONZALEZ MIGUEL ANGEL

 

Verificación de invariantes con lógica de reescritura

Alias: VerfInv-LR
Categoría: PGR1

Línea de investigación:

Objetivo general: Analizar un sistema complejo de software por medio de la lógica de reescritura.

Objetivos específicos:

  • Especificar un sistema complejo de software utilizando el enfoque algebraico de la lógica de reescritura.

  • Modelar en el lenguaje de programación Maude un sistema formal de software complejo.

  • Implementar y ejecutar pruebas de alcanzabilidad para demostrar propiedades

Logros:

  • Especificación formal
  • Simulación formal del sistema
  • Análisis de invariantes.